{nilpotent,of_associative}): a representation of an associative algebra gives a representation of a Lie algebra (#11558)

Commit

3 years ago

feat(algebra/lie/{nilpotent,of_associative}): a representation of an associative algebra gives a representation of a Lie algebra (#11558) The lemma `lie_algebra.non_trivial_center_of_is_nilpotent` is unrelated.

Author

ocfnash

Parents

99608cc6

mathlib f5b11ad5 - feat(algebra/lie/{nilpotent,of_associative}): a representation of an associative algebra gives a representation of a Lie algebra (#11558)

mathlib
f5b11ad5 - feat(algebra/lie/{nilpotent,of_associative}): a representation of an associative algebra gives a representation of a Lie algebra (#11558)