Commit 2019-11-12 15:22 14435eb2

View on Github →

feat(algebra/lie_algebra): Define lie algebras (#1644)

feat(algebra/module): define abbreviation module.End The algebra of endomorphisms of a module over a commutative ring.
feat(ring_theory/algebra): define algebra structure on square matrices over a commutative ring
feat(algebra/lie_algebras.lean): define Lie algebras
feat(algebra/lie_algebras.lean): simp lemmas for Lie rings Specifically:
- zero_left
- zero_right
- neg_left
- leg_right
feat(algebra/lie_algebras): more simp lemmas for Lie rings Specifically:
- gsmul_left
- gsmul_right
style(algebra/lie_algebras): more systematic naming
Update src/algebra/lie_algebras.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/algebra/lie_algebras.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/algebra/lie_algebras.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/algebra/lie_algebras.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/algebra/lie_algebras.lean Catch up with renaming in recent Co-authored commits
Rename src/algebra/lie_algebras.lean --> src/algebra/lie_algebra.lean
Place lie_ring simp lemmas into global namespace
Place lie_smul simp lemma into global namespace
Drop now-redundant namespace qualifiers
Update src/algebra/lie_algebra.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com
Update src/algebra/lie_algebra.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com
Catch up after recent Co-authored commits making carrier types implicit
Add missing docstrings
feat(algebra/lie_algebra): replace instance definitions with vanilla defs
style(algebra/lie_algebra): Apply suggestions from code review Co-Authored-By: Patrick Massot
Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin johan@commelin.net
Minor tidy ups