Commit 2021-11-10 02:49 3f173e11

View on Github →

feat(group_theory/complement): iff-lemmas for when bottom and top subgroups are complementary (#10143) Adds iff lemmas for when bottom and top subgroups are complementary.

Estimated changes

Modified src/data/set/basic.lean

modified theorem set.eq_singleton_iff_nonempty_unique_mem

modified theorem set.eq_singleton_iff_unique_mem

added theorem set.exists_eq_singleton_iff_nonempty_unique_mem

Modified src/group_theory/complement.lean

added theorem subgroup.is_complement'_bot_left

added theorem subgroup.is_complement'_bot_right

added theorem subgroup.is_complement'_bot_top

added theorem subgroup.is_complement'_top_bot

added theorem subgroup.is_complement'_top_left

added theorem subgroup.is_complement'_top_right

added theorem subgroup.is_complement_singleton_left

added theorem subgroup.is_complement_singleton_right

modified theorem subgroup.is_complement_singleton_top

added theorem subgroup.is_complement_top_left

added theorem subgroup.is_complement_top_right

modified theorem subgroup.is_complement_top_singleton

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.coe_eq_singleton

added theorem subgroup.coe_eq_univ