Commit 2024-06-15 15:52 7f2007a3

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/BigOperators/Group/List.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Modified Mathlib/Algebra/Module/Defs.lean

Modified Mathlib/Algebra/Order/Field/Basic.lean

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Algebra/Order/Monoid/Defs.lean

modified theorem bit0_pos

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

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

Modified Mathlib/Algebra/Order/Ring/Defs.lean

Modified Mathlib/Algebra/Ring/Commute.lean

Modified Mathlib/Algebra/Ring/Int.lean

modified theorem Int.not_even_bit1

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Iso.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

Modified Mathlib/Data/Int/Lemmas.lean

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/Data/Real/Sqrt.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Instances/Real.lean