Commit 2024-06-15 14:58 e956397c

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Ring/Rat.lean

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

Modified Mathlib/Analysis/InnerProductSpace/Calculus.lean

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Modified Mathlib/CategoryTheory/Adjunction/Over.lean

Modified Mathlib/CategoryTheory/EssentialImage.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Int/Cast/Basic.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/Data/Int/Defs.lean

modified theorem Int.ofNat_bit0

modified theorem Int.ofNat_bit1

Modified Mathlib/Data/List/InsertNth.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

Modified Mathlib/Data/Nat/Cast/Defs.lean

Modified Mathlib/Data/Num/Basic.lean

Modified Mathlib/Data/PNat/Basic.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

Modified Mathlib/Data/Rat/Defs.lean

Modified Mathlib/FieldTheory/IntermediateField.lean

Modified Mathlib/Init/Data/List/Lemmas.lean

Modified Mathlib/Init/ZeroOne.lean

modified def bit0

modified def bit1

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

Modified Mathlib/NumberTheory/SumFourSquares.lean

Modified Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.comap_le_comap

deleted theorem Filter.map_le_map

added theorem GCongr.Filter.comap_le_comap

added theorem GCongr.Filter.map_le_map

Modified Mathlib/RingTheory/Derivation/Basic.lean

Modified Mathlib/RingTheory/Flat/Basic.lean

Modified Mathlib/RingTheory/Noetherian.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

Modified Mathlib/RingTheory/SimpleModule.lean

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

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

Modified Mathlib/Topology/GDelta.lean

Modified Mathlib/Topology/MetricSpace/Completion.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean