Commit 2024-06-04 13:47 765f7e60

View on Github →

chore: add dates to more deprecations (#13186) And reformat nearby deprecations in the same file to use since syntax.

Estimated changes

Modified Mathlib/Algebra/CharP/Reduced.lean

Modified Mathlib/Algebra/Order/Group/Abs.lean

Modified Mathlib/Algebra/Squarefree/Basic.lean

Modified Mathlib/Data/DFinsupp/Basic.lean

Modified Mathlib/Data/ENNReal/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Fintype/Order.lean

Modified Mathlib/Data/Int/Defs.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/Num/Basic.lean

modified def castNum

modified def castPosNum

modified def castZNum

Modified Mathlib/Data/Option/Defs.lean

Modified Mathlib/Data/Rat/Defs.lean

modified theorem Rat.divInt_zero_one

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Init/Function.lean