Commit 2024-05-31 08:22 48de2e85

View on Github →

feat(Algebra/Lie/InvariantForm): Lie algebras with a nondegenerate invariant form are semisimple (#13391)

depends on: #13387

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/InvariantForm.lean

added theorem LieAlgebra.InvariantForm.atomistic

added theorem LieAlgebra.InvariantForm.isSemisimple_of_nondegenerate

added theorem LieAlgebra.InvariantForm.mem_orthogonal

added def LieAlgebra.InvariantForm.orthogonal

added theorem LieAlgebra.InvariantForm.orthogonal_disjoint

added theorem LieAlgebra.InvariantForm.orthogonal_isCompl

added theorem LieAlgebra.InvariantForm.orthogonal_isCompl_coe_submodule

added theorem LieAlgebra.InvariantForm.orthogonal_toSubmodule

added theorem LieAlgebra.InvariantForm.restrict_nondegenerate

added theorem LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate

added def LinearMap.BilinForm.lieInvariant

added theorem LinearMap.BilinForm.lieInvariant_iff

Modified docs/references.bib