English
A submodule inside the span of a linear independent family is free of finite rank, provided the ring is a PID; there is a Smith normal form version of this statement that does not require one to map into a fixed O first.
Русский
Подмодуль внутри оболочки линейно независимой семьи свободен и имеет конечный ранг, если кольцо является PID; существует версия в Smith нормальной форме, не требующая явного отображения в фиксированное O.
LaTeX
$$$\\text{basisOfPidOfLESpan} \\; \\text{and its SNF version exists}$$$
Lean4
/-- A submodule inside the span of a linear independent family is a free `R`-module of finite rank,
if `R` is a principal ideal domain. -/
noncomputable def basisOfPidOfLESpan {ι : Type*} [Finite ι] {b : ι → M} (hb : LinearIndependent R b) {N : Submodule R M}
(le : N ≤ Submodule.span R (Set.range b)) : Σ n : ℕ, Basis (Fin n) R N :=
Submodule.basisOfPidOfLE le (Basis.span hb)
