Theorem Set.rangeFactorization_injective

Modification history

2025-10-27 02:53

Mathlib/Data/Set/Operations.lean

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

Added Set.rangeFactorization_injective View on Github →