multiplicity_sub_multiplicity — Mathlib

English

For any q ≠ 0, padicValRat p q equals the difference of the multiplicities: multiplicity(p:ℤ) q.num − multiplicity p q.den.

Русский

Для любого q ≠ 0 p‑адическая оценка q равна разности кратностей: multiplicity(p:ℤ) q.num − multiplicity p q.den.

LaTeX

$$$\mathrm{padicValRat}(p,q) = \mathrm{multiplicity}(p:\mathbb{Z})\,q.num - \mathrm{multiplicity}\,p\,q.den$ при $hp: p\neq 1$, $hq: q\neq 0$$$

Lean4

theorem multiplicity_sub_multiplicity {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
    padicValRat p q = multiplicity (p : ℤ) q.num - multiplicity p q.den := by
  rw [padicValRat, padicValInt.of_ne_one_ne_zero hp (Rat.num_ne_zero.2 hq), padicValNat_def' hp q.den_ne_zero]

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