English
From a submodule N ⊆ M with a basis b of N, and a vector y ∈ M satisfying independence from N and spanning M together with N, there exists a basis Fin(n+1) for M given by Fin.cons y (N.subtype ∘ b).
Русский
Из подмодуля N ⊆ M и базиса b N, а также вектора y ∈ M, удовлетворяющего независимости от N и порождающего вместе с N весь M, существует базис Fin(n+1) для M, заданный Fin.cons y (N.subtype ∘ b).
LaTeX
$$$\exists b' : \Basis(\mathrm{Fin}(n+1))\, R\, M \,\text{ such that } b' = \mathrm{Fin.cons}(y, N.\text{subtype} \circ b).$$$
Lean4
@[simp]
theorem coe_mkFinCons {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R N)
(hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z : M, ∃ c : R, z + c • y ∈ N) :
(mkFinCons y b hli hsp : Fin (n + 1) → M) = Fin.cons y ((↑) ∘ b) :=
by
unfold mkFinCons
exact coe_mk (v := Fin.cons y (N.subtype ∘ b)) _ _
