ofFinite — Mathlib

English

There is a noncanonical representation of a finite R-module as a quotient of a free module R^n by a submodule S.

Русский

Существует неканоническое представление конечного R-модуля как фактор-модуля R^n / S, где S ≤ R^n.

LaTeX

$$$\text{There exists } n, S \le R^n \text{ with } M \cong_R R^n / S\;\text{ for a finite } R\text{-module }M$$$

Lean4

/-- A non-canonical representation of a finite module (as a quotient of $$R^n$$). -/
noncomputable def ofFinite : FGModuleRepr R
    where
  n := (Module.Finite.exists_fin_quot_equiv R M).choose
  S := (Module.Finite.exists_fin_quot_equiv R M).choose_spec.choose

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