English
The norm intNorm on the integer set K descends to a well-defined function on the quotient of integerSet(K) by the torsion subgroup of units. In other words, intNorm is constant on torsion orbits, so there exists a map quotIntNorm from the quotient set to the natural numbers given by quotIntNorm([a]) = intNorm(a).
Русский
Норма intNorm на множествах целых элементов K определяет корректный отображение на частный набор, полученный делением integerSet(K) по подгруппе torsion(K). Другими словами, intNorm одинаков на орбитах по действию торов; существует отображение quotIntNorm: quotient(...) → ℕ с quotIntNorm([a]) = intNorm(a).
LaTeX
$$$\\quotIntNorm: \\operatorname{Quotient}(\\operatorname{MulAction.orbitRel}(\\operatorname{torsion} K, \\operatorname{integerSet} K)) \\to \\mathbb{N}, \\quad \\quotIntNorm(\\overline{a}) = \\operatorname{intNorm}(a).$$$
Lean4
/-- The norm `intNorm` lifts to a function on `integerSet K` modulo `torsion K`. -/
def quotIntNorm : Quotient (MulAction.orbitRel (torsion K) (integerSet K)) → ℕ :=
Quotient.lift (fun x ↦ intNorm x) fun a b ⟨u, hu⟩ ↦ by
rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe, norm_unit_smul]
