Commit 2025-10-27 02:53 88d330e1

View on Github →

feat: characterise when Set.rangeFactorization is injective (#30126)

Estimated changes

Modified Mathlib/Data/Set/Image.lean

deleted theorem Set.rangeFactorization_surjective

Modified Mathlib/Data/Set/Operations.lean

added theorem Set.rangeFactorization_bijective

added theorem Set.rangeFactorization_injective

added theorem Set.rangeFactorization_surjective