Theorems · Theorem · functional analysis

LinearIsometryEquiv.reflections_generate_dim_aux

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

An element φ of the orthogonal group of F can be factored as a product of reflections, and specifically at most as many reflections as the dimension of the complement of the fixed subspace of φ.

Defined in

Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensional