finite_of_module_finite — Mathlib

English

If S is finite as an R-module, then the residue-field extension κ(R) → κ(S) is finite: κ(R) is a finite substructure of κ(S).

Русский

Если S как R-модуль конечен, то расширение полей остатка κ(R) → κ(S) конечно (κ(S) является конечным κ(R)-модулем).

LaTeX

$$[Module.Finite R S] ⇒ [Module.Finite (ResidueField R) (ResidueField S)]$$

Lean4

instance finite_of_module_finite [Module.Finite R S] : Module.Finite (ResidueField R) (ResidueField S) :=
  .of_restrictScalars_finite R _ _

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