Commit 2024-02-12 17:24 64edf019

View on Github →

feat: the pairing of a Lie algebra root space with its negative (#10454)

Estimated changes

Modified Mathlib/Algebra/Lie/Basic.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

added def LieModuleHom.codRestrict

added theorem LieModuleHom.codRestrict_apply

Modified Mathlib/Algebra/Lie/Weights/Cartan.lean

added theorem LieAlgebra.coe_rootSpaceProductNegSelf_apply

added theorem LieAlgebra.mem_range_rootSpaceProductNegSelf

added def LieAlgebra.rootSpaceProductNegSelf

Modified Mathlib/Logic/Basic.lean

added theorem exists_exists_exists_and_eq