Mathlib Changelog
v4
Changelog
About
Github
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