Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-03 11:42 18e7f914

View on Github →

feat(group_theory/quotient_group): if a quotient is trivial then the subgroup is the whole group (#9092)

Estimated changes

Modified src/data/setoid/basic.lean

added theorem quot.subsingleton_iff

added theorem quotient.subsingleton_iff

added theorem setoid.bot_def

added theorem setoid.eq_top_iff

added theorem setoid.top_def

Modified src/group_theory/quotient_group.lean

added theorem quotient_group.subgroup_eq_top_of_subsingleton

added theorem quotient_group.subsingleton_quotient_top

Modified src/logic/relation.lean

added theorem relation.eqv_gen_eq_of_equivalence