Two dimensional Euclidean spaces

This file proves that the composition of two reflections is a rotation.

Main statements

• Coxeter.reflect_reflect

theorem Coxeter.cos_two_nsmul (θ : Real.Angle) : (2 • θ).cos = θ.cos * θ.cos - θ.sin * θ.sin

instance Coxeter.instFiniteDimensionalReal_coxeter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [hdim2 : Fact (Module.finrank ℝ E = 2)] : FiniteDimensional ℝ E

noncomputable def Coxeter.reflect {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [hdim2 : Fact (Module.finrank ℝ E = 2)] {x : E} (hx : ‖x‖ = 1) : E ≃ₗ[ℝ] E

Equations

• Coxeter.reflect hx = Module.reflection ⋯

theorem Coxeter.reflect_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [hdim2 : Fact (Module.finrank ℝ E = 2)] {x : E} (hx : ‖x‖ = 1) (y : E) : (reflect hx) y = y - (2 * inner ℝ x y) • x

theorem Coxeter.reflect_reflect {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [hdim2 : Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : reflect hx ≪≫ₗ reflect hy = ↑(o.rotation (2 • o.oangle x y))

theorem Coxeter.reflect_reflect_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [hdim2 : Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (v : E) : (reflect hy) ((reflect hx) v) = (o.rotation (2 • o.oangle x y)) v

theorem Coxeter.rotation_inj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [hdim2 : Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : Function.Injective o.rotation

theorem Coxeter.rotation_pow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [hdim2 : Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (n : ℕ) (θ : Real.Angle) : o.rotation θ ^ n = o.rotation (n • θ)

theorem Coxeter.addOrderOf_two_pi_div (m : ℕ) (hm : m > 0) : addOrderOf ↑(2 * Real.pi / ↑m) = m

theorem Coxeter.order_rotation_two_pi_div {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [hdim2 : Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (m : ℕ) (hm : m > 0) : orderOf (o.rotation ↑(2 * Real.pi / ↑m)) = m