# The additive circle as a normed group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the normed group structure on add_circle p, for p : ℝ. For example if p = 1 then: ‖(x : add_circle 1)‖ = |x - round x| for any x : ℝ (see unit_add_circle.norm_eq).

## Main definitions: #

• add_circle.norm_eq: a characterisation of the norm on add_circle p

## TODO #

• The fact inner_product_geometry.angle (real.cos θ) (real.sin θ) = ‖(θ : real.angle)‖
@[protected, instance]
Equations
@[simp]
theorem add_circle.norm_coe_mul (p x t : ) :
@[simp]
theorem add_circle.norm_eq (p : ) {x : } :
theorem add_circle.norm_eq' (p : ) (hp : 0 < p) {x : } :
theorem add_circle.norm_le_half_period (p : ) {x : add_circle p} (hp : p 0) :
@[simp]
theorem add_circle.norm_half_period_eq (p : ) :
(p / 2) = |p| / 2
theorem add_circle.norm_coe_eq_abs_iff (p : ) {x : } (hp : p 0) :
theorem add_circle.closed_ball_eq_univ_of_half_period_le (p : ) (hp : p 0) (x : add_circle p) {ε : } (hε : |p| / 2 ε) :
theorem add_circle.coe_real_preimage_closed_ball_inter_eq (p : ) {x ε : } (s : set ) (hs : s (|p| / 2)) :
s = ite < |p| / 2) s) s
theorem add_circle.norm_div_nat_cast {p : } [hp : fact (0 < p)] {m n : } :
(m / n * p) = p * ((linear_order.min (m % n) (n - m % n)) / n)