Commit 2024-06-10 14:50 9c332554
View on Github →chore: move and generalize card_fiber_eq_of_mem_range (#10088)
This PR moves the lemma card_fiber_eq_of_mem_range from RingTheory/IntegralDomain to GroupTheory/Index which makes far more sense. It also adds the additive version, generalizes to MonoidHomClass, and puts it in the MonoidHom namespace (instead of root).