addVal_def — Mathlib

English

If r = u · ϖ^n for a unit u and irreducible ϖ, then the additive valuation addVal(r) equals n.

Русский

Если элемент r записывается как r = u · ϖ^n, где u — единица и ϖ ирредуцируем, то addVal(r) = n.

LaTeX

$$$\mathrm{addVal}(r) = n$$$

Lean4

theorem addVal_def (r : R) (u : Rˣ) {ϖ : R} (hϖ : Irreducible ϖ) (n : ℕ) (hr : r = u * ϖ ^ n) : addVal R r = n := by
  classical
    rw [addVal, multiplicity_addValuation_apply, hr,
    emultiplicity_eq_of_associated_left
      (associated_of_irreducible R hϖ (Classical.choose_spec (exists_prime R)).irreducible),
    emultiplicity_eq_of_associated_right (Associated.symm ⟨u, mul_comm _ _⟩),
    emultiplicity_pow_self_of_prime (irreducible_iff_prime.1 hϖ)]

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