ne_bot — Mathlib

English

If P lies over p in a Dedekind extension, and p ≠ ⊥, then the ramification index e over p to P is nonzero.

Русский

Если P лежит над p в расширении Дедеклина и p ≠ ⊥, то рамфикационный индекс над p к P ненулевой.

LaTeX

$$$\\\\operatorname{ramificationIdx} (\\\\text{algebraMap } R S) p P \\\\neq 0$$$

Lean4

theorem ne_bot (P : (factors (map (algebraMap R S) p)).toFinset) : (P : Ideal S) ≠ ⊥ :=
  (prime_of_factor _ (Multiset.mem_toFinset.mp P.2)).ne_zero

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