English
For a basis b and i ∈ ι, and f : ι →₀ R, the i-th coordinate of b.repr.symm f equals f i.
Русский
Для базиса b, i ∈ ι, и f : ι →₀ R координата i в b.repr.symm f равна f i.
LaTeX
$$$ b.coord\,i (b.repr.symm\ f) = f(i) $$$
Lean4
/-- Let `b` be a basis for a submodule `N ≤ O`. If `y ∈ O` is linear independent of `N`
and `y` and `N` together span the whole of `O`, then there is a basis for `O`
whose basis vectors are given by `Fin.cons y b`. -/
noncomputable def mkFinConsOfLE {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R N) (hNO : N ≤ O)
(hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ c : R, z + c • y ∈ N) :
Basis (Fin (n + 1)) R O :=
mkFinCons ⟨y, yO⟩ (b.map (Submodule.comapSubtypeEquivOfLe hNO).symm)
(fun c x hc hx => hli c x (Submodule.mem_comap.mp hc) (congr_arg ((↑) : O → M) hx)) fun z => hsp z z.2
