def
definition
oneDimSubspace
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Algebra.F2Power on GitHub at line 241.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
238unique. -/
239
240/-- The 1-dimensional subspace generated by a non-zero `v`. -/
241def oneDimSubspace (v : F2Power D) : Finset (F2Power D) :=
242 {0, v}
243
244theorem oneDimSubspace_card (v : F2Power D) (hv : v ≠ 0) :
245 (oneDimSubspace v).card = 2 := by
246 unfold oneDimSubspace
247 simp [Finset.card_insert_of_notMem, Ne.symm hv]
248
249/-- The 1-dimensional subspace is closed under addition. -/
250theorem oneDimSubspace_closed (v : F2Power D) (a b : F2Power D)
251 (ha : a ∈ oneDimSubspace v) (hb : b ∈ oneDimSubspace v) :
252 a + b ∈ oneDimSubspace v := by
253 unfold oneDimSubspace at ha hb ⊢
254 simp [Finset.mem_insert, Finset.mem_singleton] at ha hb ⊢
255 rcases ha with ha | ha <;> rcases hb with hb | hb <;>
256 subst_vars <;> simp [add_self]
257
258end F2Power
259
260end Algebra
261end IndisputableMonolith