ramificationIdx_ne_zero — Mathlib

English

If e ≠ 0 and ramificationIdx f p P ≠ 0, then map f p ≤ P^e and the ramification index is determined by e.

Русский

Если e ≠ 0 и ramificationIdx f p P ≠ 0, то map f p ≤ P^e и индекс рамификации определяется по e.

LaTeX

$$$\\forall e:\\mathbb{N}, e\\neq 0 \\to\\Big( map f p ≤ P^e \\land ramificationIdx f p P ≠ 0 \\Rightarrow \\text{условие}\Big)$$$

Lean4

theorem ramificationIdx_ne_zero {e : ℕ} (he : e ≠ 0) (hle : map f p ≤ P ^ e) (hnle : ¬map f p ≤ P ^ (e + 1)) :
    ramificationIdx f p P ≠ 0 := by rwa [ramificationIdx_spec hle hnle]

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