Commit 2025-03-02 22:57 3814166c

View on Github →

chore(Interval/Set/Basic): add @[simp] and @[gcongr] attrs (#22453)

Estimated changes

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Order/Interval/Finset/Basic.lean

Modified Mathlib/Order/Interval/Set/Basic.lean

Modified Mathlib/Order/SuccPred/Basic.lean

modified theorem Order.Ici_subset_Ioi_pred

modified theorem Order.Iic_subset_Iio_succ