Endomorphisms

• Orthogonal group
• Unitary group
• Special orthogonal group
• Special unitary group
• Self-adjoint endomorphism

ClassNormal endomorphism#

An element of a star monoid is normal if it commutes with its adjoint.

IsStarNormal.{u_1} {R : Type u_1} [Mul R] [Star R] (x : R) : Prop

Sources

• Mathlib documentation: IsStarNormal
• Source of IsStarNormal in Mathlib/Algebra/Star/SelfAdjoint.lean
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Endomorphisms

MathlibIsStarNormal

• Diagonalization of a self-adjoint endomorphism

TheoremDecomposition of an orthogonal transformation as a product of reflections#

The orthogonal group of F is generated by reflections.

LinearIsometryEquiv.reflections_generate.{u_3} {F : Type u_3} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] :
  Subgroup.closure (Set.range fun v => (ℝ ∙ v)ᗮ.reflection) = ⊤

Sources

• Mathlib documentation: LinearIsometryEquiv.reflections_generate
• Source of LinearIsometryEquiv.reflections_generate in Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Endomorphisms

MathlibLinearIsometryEquiv.reflections_generate

Uses 7

Statement usesCompactness in terms of filters · Finite-dimensionality · Reflection · Subgroup generated by a subset

Proof usesHeine-Borel theorem (finite-dimensional normed spaces are proper) · Homeomorphisms · Kernel of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.