English
For a fixed natural number n, the valuation of NeZeroMod encodes the exponents of prime factors modulo n across all units in K, forming a monoid hom from the quotient of K by n to a multiplicative ZMod n.
Русский
При фиксированном натуральном числе n оценка NeZeroMod кодирует степени простых делителей по модулю n на всех модулях в K, образуя моноидообразное отображение из фактора K по n в мультипликативный ZMod n.
LaTeX
$$$\text{valuationOfNeZeroMod}(n): (K/ n)^{\times}\to \operatorname{Multiplicative}(\mathbb{Z}/n\mathbb{Z})$$$
Lean4
@[simp]
theorem valuationOfNeZeroToFun_eq (x : Kˣ) : (v.valuationOfNeZeroToFun x : ℤᵐ⁰) = v.valuation K x := by
classical
rw [show v.valuation K x = _ * _ by rfl]
rw [Units.val_inv_eq_inv_val]
change _ = ite _ _ _ * (ite _ _ _)⁻¹
simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
if_neg <| IsLocalization.sec_fst_ne_zero x.ne_zero, if_neg (nonZeroDivisors.coe_ne_zero _), valuationOfNeZeroToFun,
ofAdd_sub, ofAdd_neg, div_inv_eq_mul, WithZero.coe_mul, WithZero.coe_inv, inv_inv]
