Commit 2023-06-05 19:04 d7599344

View on Github →

feat: port Algebra.Lie.DirectSum (#4684)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/DirectSum.lean

added theorem DirectSum.bracket_apply

added def DirectSum.lieAlgebraComponent

added def DirectSum.lieAlgebraOf

added theorem DirectSum.lieAlgebra_ext

added def DirectSum.lieModuleComponent

added def DirectSum.lieModuleOf

added theorem DirectSum.lie_module_bracket_apply

added theorem DirectSum.lie_of

added theorem DirectSum.lie_of_of_eq

added theorem DirectSum.lie_of_of_ne

added def DirectSum.toLieAlgebra