inertiaDegIn_ne_zero — Mathlib

English

Under IsGalois K L, inertiaDegIn p B = inertiaDeg p P for maximal p.

Русский

При IsGalois K L, inertiaDegIn p B = inertiaDeg p P для максимального p.

LaTeX

$$$\\mathrm{inertiaDegIn}\\ p\\ B = \\mathrm{inertiaDeg}\\ p\\ P$$$

Lean4

theorem inertiaDegIn_ne_zero {p : Ideal A} [p.IsMaximal] [IsGalois K L] [NoZeroSMulDivisors A B] :
    inertiaDegIn p B ≠ 0 := by
  obtain ⟨P⟩ := (inferInstance : Nonempty (primesOver p B))
  rw [inertiaDegIn_eq_inertiaDeg p P K L]
  exact inertiaDeg_ne_zero _ _

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