finiteQuotientOfFreeOfRankEq — Mathlib

English

A submodule of full rank of a free finite module has a finite quotient.

Русский

Подмодуль полного ранга свободного конечного модуля имеет конечный фактор-модуль.

LaTeX

$$$$ \mathrm{Finite}(M / N) $$$$

Lean4

/-- A submodule of full rank of a free finite `ℤ`-module has a finite quotient.
It can't be an instance because of the side condition `Module.finrank ℤ N = Module.finrank ℤ M`.
-/
theorem finiteQuotientOfFreeOfRankEq [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M)
    (h : Module.finrank ℤ N = Module.finrank ℤ M) : Finite (M ⧸ N) :=
  by
  let b := Module.Free.chooseBasis ℤ M
  let a := smithNormalFormCoeffs b h
  let e := N.quotientEquivPiZMod b h
  have : ∀ i, NeZero (a i).natAbs := fun i ↦ ⟨Int.natAbs_ne_zero.mpr (smithNormalFormCoeffs_ne_zero b h i)⟩
  exact Finite.of_equiv (Π i, ZMod (a i).natAbs) e.symm

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