instFiniteResidueField — Mathlib

English

If R is local and finitely generated over R0, then the residue field of R is finite over R0.

Русский

Если R локальное и конечно порождено над R0, то остаточное поле R — конечно по модулю R0.

LaTeX

$$$\\text{IsLocalRing.instFiniteResidueField }\\,(R) : \\text{Module.Finite } R_0 (\\mathrm{ResidueField}(R))$$$

Lean4

instance {R₀} [CommRing R₀] [Algebra R₀ R] [Module.Finite R₀ R] : Module.Finite R₀ (ResidueField R) :=
  .of_surjective (IsScalarTower.toAlgHom R₀ R _).toLinearMap Ideal.Quotient.mk_surjective

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