Mathlib v3 is deprecated. Go to Mathlib v4

Theorem commutator_le_map_commutator

Modification history

2022-04-08 07:42
src/group_theory/solvable.lean
refactor(group_theory/commutator): Move `commutator_le_map_commutator` (#13229) …
Deleted commutator_le_map_commutatorView on Github →
2021-01-07 19:12
src/group_theory/solvable.lean
feat(group_theory): add lemmas on solvability (#5646) …
Added commutator_le_map_commutatorView on Github →