English
In a finite-dimensional real inner product space F, every φ in the orthogonal group can be expressed as a product of finitary reflections; i.e., there exists a finite list of vectors whose reflections multiply to φ.
Русский
В конечномерном вещественном пространстве с ограниченным скалярным произведением каждый φ в ортогональной группе может быть записан как произведение конечного числа отражений; есть конечный список векторов, отражения по которым составляют φ.
LaTeX
$$$\\exists l : \\text{List } F, l$.length ≤ finrank ℝ F ∧ φ = (l.map (fun v => (\\mathbb{R} \\cdot v)^{\\perp}.reflection).prod)$$$
Lean4
/-- The orthogonal group of `F` is generated by reflections. -/
theorem reflections_generate [FiniteDimensional ℝ F] :
Subgroup.closure (Set.range fun v : F => reflection (ℝ ∙ v)ᗮ) = ⊤ :=
by
rw [Subgroup.eq_top_iff']
intro φ
rcases φ.reflections_generate_dim with ⟨l, _, rfl⟩
apply (Subgroup.closure _).list_prod_mem
intro x hx
rcases List.mem_map.mp hx with ⟨a, _, hax⟩
exact Subgroup.subset_closure ⟨a, hax⟩
