The additive circle as a normed group #
We define the normed group structure on AddCircle p
, for p : ℝ
. For example if p = 1
then:
‖(x : AddCircle 1)‖ = |x - round x|
for any x : ℝ
(see UnitAddCircle.norm_eq
).
Main definitions: #
AddCircle.norm_eq
: a characterisation of the norm onAddCircle p
TODO #
- The fact
InnerProductGeometry.angle (Real.cos θ) (Real.sin θ) = ‖(θ : Real.Angle)‖
@[simp]
theorem
AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder
{p : ℝ}
[hp : Fact (0 < p)]
{u : AddCircle p}
(hu : IsOfFinAddOrder u)
(hu' : u ≠ 0)
: