Commit 2024-06-12 15:03 effa9ce4

View on Github →

chore(*): more since := in deprecated (#13743)

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.succAbove_lt_ge

Modified Mathlib/Data/Int/Bitwise.lean

Modified Mathlib/Data/Matrix/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

Modified Mathlib/Topology/Order.lean

Modified Mathlib/Topology/Order/Basic.lean

Modified Mathlib/Topology/Order/LeftRightNhds.lean