English
For natural numbers m, n, and a positive real p (in the AddCircle context), the norm of (↑m / ↑n)·p inside AddCircle(p) equals p times a rational expression determined by m, n, and the mod operation, explicitly given by min(m % n, n - m % n) / n scaled by p.
Русский
Для натуральных чисел m, n и положительного p в AddCircle(p) норма элемента (m/n)·p равна p·(min(m mod n, n - (m mod n)) / n).
LaTeX
$$$\\| (\\tfrac{\\uparrow m}{\\uparrow n} \\cdot p) \\| = p \\cdot \\dfrac{\\min(m \\bmod n, n - (m \\bmod n))}{n}$$$
Lean4
theorem norm_div_natCast {m n : ℕ} : ‖(↑(↑m / ↑n * p) : AddCircle p)‖ = p * (↑(min (m % n) (n - m % n)) / n) :=
by
have : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n := by rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]
rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]
