English
Every element φ of the real orthogonal group O(F) on a finite-dimensional real inner product space F can be written as a product of at most dim(F) reflections.
Русский
Любой элемент φ из реальной ортогональной группы O(F) действует на реалном евклидовом пространстве F как произведение не более чем из dim(F) отражений.
LaTeX
$$$\\exists l : \\text{List } F, l$.length ≤ finrank ℝ F ∧ φ = (l.map (fun v => reflection (ℝ \\cdot v)^{\\perp}).prod)$$$
Lean4
/-- The orthogonal group of `F` is generated by reflections; specifically each element `φ` of the
orthogonal group is a product of at most as many reflections as the dimension of `F`.
Special case of the **Cartan–Dieudonné theorem**. -/
theorem reflections_generate_dim [FiniteDimensional ℝ F] (φ : F ≃ₗᵢ[ℝ] F) :
∃ l : List F, l.length ≤ finrank ℝ F ∧ φ = (l.map fun v => reflection (ℝ ∙ v)ᗮ).prod :=
let ⟨l, hl₁, hl₂⟩ := φ.reflections_generate_dim_aux le_rfl
⟨l, hl₁.trans (finrank_le _), hl₂⟩
