ramificationIdx_eq_find — Mathlib

English

Under a ring equivalence e, the ramification index computed after mapping p to P matches the ramification index computed after mapping p to P under the corresponding transported rings.

Русский

При эквивалентности колец e расход ramificationIdx сохраняется при отображении p в P через перенесённые кольца.

LaTeX

$$$ramificationIdx(\\text{algebraMap } R S, p, P) = ramificationIdx(\\text{algebraMap } R S_1, p, P)$$$

Lean4

theorem ramificationIdx_eq_find [DecidablePred fun n ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n]
    (h : ∃ n, ∀ k, map f p ≤ P ^ k → k ≤ n) : ramificationIdx f p P = Nat.find h := by convert Nat.sSup_def h

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