mathlib
12c868a5 - refactor(group_theory/complement): Generalize `card_mul` to from subgroups to subsets (#10264)

Commit

4 years ago

refactor(group_theory/complement): Generalize `card_mul` to from subgroups to subsets (#10264) Adds `is_complement.card_mul`, which generalizes `is_complement'.card_mul`.

Author

tb65536

Parents

72ca0d33

mathlib 12c868a5 - refactor(group_theory/complement): Generalize `card_mul` to from subgroups to subsets (#10264)

mathlib
12c868a5 - refactor(group_theory/complement): Generalize `card_mul` to from subgroups to subsets (#10264)