English
Fix a basis e. For any family v: ι → M, the pair LinearIndependent v and span equal to the whole space is equivalent to the determinant e.det v being a unit in R.
Русский
Пусть фиксирован базис e. Для любой семейства v: ι → M равенство линейной независимости и полный охват пространства эквивалентны тому, что det_e(v) является единицей в R.
LaTeX
$$LinearIndependent R v ∧ span R (range v) = ⊤ ↔ IsUnit (e.det v)$$
Lean4
theorem is_basis_iff_det {v : ι → M} : LinearIndependent R v ∧ span R (Set.range v) = ⊤ ↔ IsUnit (e.det v) :=
by
constructor
· rintro ⟨hli, hspan⟩
set v' := Basis.mk hli hspan.ge
rw [e.det_apply]
convert LinearEquiv.isUnit_det (LinearEquiv.refl R M) v' e using 2
ext i j
simp [v']
· intro h
rw [Basis.det_apply, Basis.toMatrix_eq_toMatrix_constr] at h
set v' := Basis.map e (LinearEquiv.ofIsUnitDet h) with v'_def
have : ⇑v' = v := by
ext i
rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]
rw [← this]
exact ⟨v'.linearIndependent, v'.span_eq⟩
