Theorem Set.rangeFactorization_bijective

Modification history

2025-10-27 02:53

Mathlib/Data/Set/Operations.lean

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

Added Set.rangeFactorization_bijective View on Github →