mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(ring_theory/integral_domain): generalize `card_fiber_eq_of_mem_range`

Open urkud opened this issue 2 years ago • 0 comments

  • Generalize card_fiber_eq_of_mem_range to homomorphisms from a group to a monoid.
  • Rename it to monoid_hom.card_fiber_eq_of_mem_range, use to_additive.

Open in Gitpod

urkud avatar Nov 20 '22 20:11 urkud