inertiaDeg_ne_zero — Mathlib

English

If p is maximal, S is finite over R, and P lies over p, then inertiaDeg(p,P) is nonzero; in particular the residue extension is nontrivial.

Русский

Если p максимален, S конечно над R и P лежит над p, то inertiaDeg(p,P) не равно нулю, следовательно, поле остатков расширяется ненулево.

LaTeX

$$$0 < \\operatorname{inertiaDeg} \\, p \\, P$$$

Lean4

theorem inertiaDeg_ne_zero [p.IsMaximal] [Module.Finite R S] [P.LiesOver p] : inertiaDeg p P ≠ 0 :=
  (Nat.ne_of_lt (inertiaDeg_pos p P)).symm

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