basisOfPid — Mathlib

English

Given a basis b for M and a submodule N, one can choose a finite index n and a basis for N with respect to Fin n.

Русский

Имея базис b для M и подмодуль N, можно выбрать конечный индекс n и базис для N по Fin n.

LaTeX

$$$\\exists n\\; \\exists b_N: Basis (Fin n) R N$$$

Lean4

/-- A submodule of a free `R`-module 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.smithNormalForm`.
-/
noncomputable def basisOfPid {ι : Type*} [Finite ι] (b : Basis ι R M) (N : Submodule R M) :
    Σ n : ℕ, Basis (Fin n) R N :=
  ⟨_, (N.nonempty_basis_of_pid b).choose_spec.some⟩

Похожие утверждения