Revision #2933 → #3454 · back to history
modifiedCommutator Lie algebra from an associative algebra0460518f321a
| Field | From #2933 | To #3454 |
|---|
| mathlib.decl | LieAlgebra.ofAssociativeAlgebra | LieRing.ofAssociativeRing |
| note | `LieAlgebra.ofAssociativeAlgebra` gives every associative algebra a Lie algebra instance via the ring commutator. | Every associative ring/algebra carries a `LieRing` instance whose bracket is the commutator (`LieRing.ofAssociativeRing`). |
| provenance | ai | ai-moderated |
modifiedFundamental example: linear maps of a vector space7359f01f0832
| Field | From #2933 | To #3454 |
|---|
| note | `Module.End R V` is a ring, hence a Lie algebra via the `LieRing.ofAssociativeRing`/`LieAlgebra.ofAssociativeAlgebra` commutator instance. | `Module.End R V` is a ring, hence a Lie algebra via the `LieRing.ofAssociativeRing` commutator instance. |
addedLower central series88c7c85631bf
addedDerived series102f44e05722
addedComplexification of a real Lie algebra468c83926ce1