Commit 2022-03-10 04:56 ef25c4ca

View on Github →

refactor(group_theory/commutator): Rename commutator_containment to commutator_mem_commutator (#12553) This PR renames commutator_containment to commutator_mem_commutator, uses the new commutator notation, and makes the subgroups implicit.

Estimated changes

Modified src/group_theory/commutator.lean

deleted theorem subgroup.commutator_containment

added theorem subgroup.commutator_mem_commutator

Modified src/group_theory/nilpotent.lean

Modified src/group_theory/solvable.lean