English
Definition of a mod-n valuation on K× via quotient by zmultiples and localization maps, compatible with valuationOfNeZero.
Русский
Определение mода-n оценки на K× через факторы zmultiples и локализационные отображения, совместимое с valuationOfNeZero.
LaTeX
$$def valuationOfNeZeroMod (n : Nat) : (K / n) →* Multiplicative (ZMod n)$$
Lean4
/-- The multiplicative `v`-adic valuation on `Kˣ` modulo `n`-th powers. -/
def valuationOfNeZeroMod (n : ℕ) : (K / n) →* Multiplicative (ZMod n) :=
-- TODO: this definition does a lot of defeq abuse between `Multiplicative` and `Additive`,
-- so we need `erw` below.
(Int.quotientZMultiplesNatEquivZMod n).toMultiplicative.toMonoidHom.comp <|
QuotientGroup.map (powMonoidHom n : Kˣ →* Kˣ).range (AddSubgroup.toSubgroup (AddSubgroup.zmultiples (n : ℤ)))
v.valuationOfNeZero
(by
rintro _ ⟨x, rfl⟩
exact ⟨v.valuationOfNeZero x, by simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]; rfl⟩)
