Commit 2024-06-11 22:52 a43df3c4

View on Github →

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

Estimated changes

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Order/Cover.lean

Modified Mathlib/Order/Filter/Germ.lean

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/Noetherian.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/PartENat.lean

Modified Mathlib/SetTheory/Lists.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

Modified Mathlib/Topology/Algebra/WithZeroTopology.lean

modified theorem WithZeroTopology.t3Space

Modified Mathlib/Topology/Compactness/Compact.lean

modified theorem Nat.cocompact_eq

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

Modified Mathlib/Topology/Instances/EReal.lean

Modified Mathlib/Topology/Instances/Irrational.lean