mathlib3
6cd63207 - feat(group_theory/complement): `is_complement'.sup_eq_top` (#10230)

Commit

4 years ago

feat(group_theory/complement): `is_complement'.sup_eq_top` (#10230) If `H` and `K` are complementary subgroups, then `H ⊔ K = ⊤`.

Author

tb65536

Parents