instModuleFinite — Mathlib

English

If E is a finite R-module, then WithCStarModule A E is also a finite R-module.

Русский

Если E — конечный как модуль над R, то и WithCStarModule A E является конечным R-модулем.

LaTeX

$$$ \text{Module.Finite}_R\bigl(C⋆ᵐᵒᵈ(A,E)\bigr) \text{ whenever } \text{Module.Finite}_R(E)$$$

Lean4

instance instModuleFinite [Semiring R] [AddCommGroup E] [Module R E] [Module.Finite R E] :
    Module.Finite R C⋆ᵐᵒᵈ(A, E) :=
  ‹Module.Finite R E›

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