English
For submodules N ≤ O inside a free module M, there exists a decomposition of N as a submodule of M that respects the inclusion into O via a basis relative to the embedding of N into O.
Русский
Для подмодулей N ≤ O внутри свободного модуля M существует разложение N как подмодуля M, совместимое с включением в O через базис относительно вложения N в O.
LaTeX
$$$\\exists n, Basis (Fin n) R N$ with compatibility through a le and a Basis for O$$
Lean4
/-- A submodule inside a free `R`-submodule of finite rank is also a free `R`-module of finite rank,
if `R` is a principal ideal domain.
See also the stronger version `Submodule.smithNormalFormOfLE`.
-/
noncomputable def basisOfPidOfLE {ι : Type*} [Finite ι] {N O : Submodule R M} (hNO : N ≤ O) (b : Basis ι R O) :
Σ n : ℕ, Basis (Fin n) R N :=
let ⟨n, bN'⟩ := Submodule.basisOfPid b (N.comap O.subtype)
⟨n, bN'.map (Submodule.comapSubtypeEquivOfLe hNO)⟩
