mathlib3
fe76b5c0 - feat(group_theory/subgroup/basic): `mul_mem_sup` (#10007)

Commit
4 years ago
feat(group_theory/subgroup/basic): `mul_mem_sup` (#10007) Adds `mul_mem_sup` and golfs a couple proofs that reprove this result.
Author
Parents
Loading