map_one' — Mathlib

English

Let v be a height-one spectrum valuation on a Dedekind domain R. Then the v-adic valuation of 1 is 1.

Русский

Пусть v — оценка на дедекдиндовом домене R, связанная с спектром высоты 1. Тогда v-адическая величина 1 равна 1.

LaTeX

$$$v(1) = 1$$$

Lean4

/-- The `v`-adic valuation of `1 : R` equals 1. -/
theorem map_one' : v.intValuationDef 1 = 1 := by
  classical
    rw [v.intValuationDef_if_neg (zero_ne_one.symm : (1 : R) ≠ 0), Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero (by apply v.associates_irreducible),
    Int.ofNat_zero, neg_zero, ofAdd_zero, WithZero.coe_one]

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