mathlib3
1ad29d69 - refactor(algebra/lie/of_associative): remove `ring_commutator` namespace; use `ring` instead (#6181)

Commit
4 years ago
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`
Author
Parents
Loading