Theorem Set.image_of_range_union_range_eq_univ

Modification history

2025-01-24 05:43
Mathlib/Data/Set/Image.lean
feat: split a set in the prime spectrum of `R[X]` into its localization away from `c : R` and quotient by `c` parts (#20303) …
Added Set.image_of_range_union_range_eq_univView on Github →