Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 16:21 1ad29d69

View on Github →

refactor(algebra/lie/of_associative): remove ring_commutator namespace; use ring instead (#6181) The old_structure_cmd change to lie_algebra.is_simple is unrelated and is included here only for convenience. ring_commutator.commutator -> ring.lie_def

Estimated changes