Theorem QuotientGroup.card_quotient_rightRel

Modification history

2025-07-23 15:29

Mathlib/GroupTheory/Coset/Basic.lean

chore(GroupTheory/FreeAbelianGroup): do not import cardinals (#27169) …

Modified QuotientGroup.card_quotient_rightRel View on Github →

2023-01-31 10:56

Mathlib/GroupTheory/Coset.lean

feat: port GroupTheory.Coset (#1874) …

Added QuotientGroup.card_quotient_rightRel View on Github →