ramificationIdxIn_ne_zero — Mathlib

English

If p is a prime ideal in A and lies over in B with IsGalois extension, then ramificationIdxIn p B ≠ 0.

Русский

Если p – простый идеал A и существует Галуа-расширение, то ramificationIdxIn p B ≠ 0.

LaTeX

$$$\\mathrm{ramificationIdxIn\\ } p\\ B \\neq 0$$$

Lean4

theorem ramificationIdxIn_ne_zero [IsDedekindDomain B] {p : Ideal A} [p.IsPrime] (hp : p ≠ ⊥) [IsGalois K L]
    [NoZeroSMulDivisors A B] : p.ramificationIdxIn B ≠ 0 :=
  by
  obtain ⟨P⟩ := (inferInstance : Nonempty (primesOver p B))
  rw [ramificationIdxIn_eq_ramificationIdx p P K L]
  exact IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver P.1 hp

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