Revision #2289 → #2933 · back to history
modifiedCommutator Lie algebra from an associative algebra0460518f321a
| Field | From #2289 | To #2933 |
|---|
| note | An associative algebra is given a Lie algebra instance via the ring commutator bracket. | `LieAlgebra.ofAssociativeAlgebra` gives every associative algebra a Lie algebra instance via the ring commutator. |
modifiedFundamental example: linear maps of a vector space7359f01f0832
| Field | From #2289 | To #2933 |
|---|
| note | `Module.End R V` is a ring, hence a Lie algebra via the commutator instance. | `Module.End R V` is a ring, hence a Lie algebra via the `LieRing.ofAssociativeRing`/`LieAlgebra.ofAssociativeAlgebra` commutator instance. |
addedJacobi identityfcffee2661d8
modifiedCartan subalgebra7d9c2404c8f2
| Field | From #2289 | To #2933 |
|---|
| note | `IsCartanSubalgebra` is a nilpotent, self-normalizing Lie subalgebra in Mathlib. | `LieSubalgebra.IsCartanSubalgebra` is a nilpotent, self-normalizing Lie subalgebra in Mathlib. |
addedsl₂ triple43221de85f80
modifiedCartan's criterion for solvabilityfa4c328d976a
| Field | From #2289 | To #2933 |
|---|
| mathlib.decl | — | LieAlgebra.isSolvable_of_killingForm_apply_lie_eq_zero |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Algebra.Lie.CartanCriterion |
| note | The solvability half of Cartan's criterion (Killing form vanishes on [L,L]) is not formalized. | The `Killing form vanishes on [L,L] ⟹ L solvable` direction is formalized (in char 0); the converse is an explicit TODO in the file. |
| status | not_formalized | partial |