ofFiniteEquiv — Mathlib

English

The noncanonical representation of a finite module is isomorphic to the given module by a linear equivalence.

Русский

Неканоническое представление конечного модуля эквивалентно данному модулю линейным изоморфизмом.

LaTeX

$$$\exists e:\; (FGModuleRepr.ofFinite(R,M)) \cong_{R} M$$$

Lean4

/-- The non-canonical representation `ofFinite` of a finite module is actually isomorphic to
the given module. -/
noncomputable def ofFiniteEquiv : ofFinite R M ≃ₗ[R] M :=
  Classical.choice (Module.Finite.exists_fin_quot_equiv R M).choose_spec.choose_spec

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