Commit 2026-01-31 14:53 407f2a5a

View on Github →

chore: Rename ncard_image_of_injOn (#34589) See zulip, there are inconsistent namings.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean

Modified Mathlib/Data/Set/Card.lean

added theorem Set.InjOn.ncard_image

deleted theorem Set.ncard_image_of_injOn

Modified Mathlib/RingTheory/PowerSeries/Ideal.lean