instModuleFinite — Mathlib

English

The separation quotient of a finite module is itself a finite module.

Русский

Разделительная квота конечного модуля является конечным модулем.

LaTeX

$$$\mathrm{Module.Finite}\ R(\mathrm{SeparationQuotient}M)$$$

Lean4

/-- The separation quotient of a finite module is a finite module. -/
instance instModuleFinite {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M]
    [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] : Module.Finite R (SeparationQuotient M) :=
  Module.Finite.of_surjective (mkCLM R M).toLinearMap Quotient.mk_surjective

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