Theorem Set.Ici_one_eq_univ

Modification history

2026-07-01 06:16
Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
feat(Order): `Ici (1 : α) = univ` when `IsBotOneClass α` (#40762) …
Modified Set.Ici_one_eq_univView on Github →
2026-02-02 07:19
Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
feat(RingTheory/MvPolynomial): powers of ideal of variables (#33539) …
Added Set.Ici_one_eq_univView on Github →