norm_half_period_eq — Mathlib

English

For any real p, the element corresponding to p/2 inside AddCircle(p) has norm exactly |p|/2 (with the p = 0 case yielding 0 = 0).

Русский

Для любого числа p норма образа p/2 в AddCircle(p) равна точно |p|/2 (в случае p = 0 доказательство тривиально).

LaTeX

$$$\\| (\\tfrac{p}{2} : \\mathrm{AddCircle}(p)) \\| = \\dfrac{|p|}{2}$$$

Lean4

@[simp]
theorem norm_half_period_eq : ‖(↑(p / 2) : AddCircle p)‖ = |p| / 2 :=
  by
  rcases eq_or_ne p 0 with (rfl | hp); · simp
  rw [norm_eq, ← mul_div_assoc, inv_mul_cancel₀ hp, one_div, round_two_inv, Int.cast_one, one_mul,
    (by linarith : p / 2 - p = -(p / 2)), abs_neg, abs_div, abs_two]

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