Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quotient_group.forall_coe

Modification history

2022-10-24 07:29
src/group_theory/coset.lean
feat(group_theory/index): criterion for subgroups of index two (#16629) …
Modified quotient_group.forall_coeView on Github →
2021-12-04 01:52
src/group_theory/coset.lean
feat(*): `A ⧸ B` notation for quotients in algebra (#10501) …
Modified quotient_group.forall_coeView on Github →
2021-08-16 16:19
src/group_theory/coset.lean
feat(group_theory/nilpotent): add nilpotent groups (#8538) …
Added quotient_group.forall_coeView on Github →