Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-17 15:34 307711e2

View on Github →

feat(group_theory/general_commutator): subgroup.pi commutes with the general_commutator (#11825)

Estimated changes

Modified src/group_theory/general_commutator.lean

added theorem general_commutator_pi_pi_le

added theorem general_commutator_pi_pi_of_fintype

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.le_pi_iff

added theorem subgroup.pi_eq_bot_iff

added theorem subgroup.pi_le_iff

added theorem subgroup.pi_mem_of_single_mem

added theorem subgroup.pi_mem_of_single_mem_aux

added theorem subgroup.single_mem_pi