instFormallyUnramifiedResidueField_1

English

If R,S are local and unramified with EssFiniteType, then the residue fields form a finite module over each other.

Русский

Если R,S локальны и неразветвлены и имеют EssFiniteType, то поля Остатка образуют конечное расширение друг друга.

LaTeX

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

Lean4

instance [FormallyUnramified R S] : FormallyUnramified (ResidueField R) (ResidueField S) :=
  have : FormallyUnramified R (ResidueField S) := .comp _ S _
  .of_comp R _ _

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