Theorems · Theorem · functional analysis

LinearIsometryEquiv.reflections_generate_dim

∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [FiniteDimensional ℝ F]
  (φ : F ≃ₗᵢ[ℝ] F), ∃ l, l.length ≤ Module.finrank ℝ F ∧ φ = (List.map (fun v => (ℝ ∙ v)ᗮ.reflection) l).prod

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.

Defined in

Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Cited by

1 results in Mathlib

Foundations

Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensional