Commit 2024-05-07 01:05 21b3a48b

View on Github →

refactor: replace @[reducible] with abbrev (#12614) A test to see how many uses of @[reducible] in Mathlib can be replaced with abbrev. TODOs:

  • @[to_additive (attr := reducible)] def
  • attribute [reducible] ConcreteCategory.forget

Estimated changes

deleted def Arithcc.Identifier
deleted def Arithcc.Register
deleted def Arithcc.Word
deleted def Algebra.ofModule'
deleted def Algebra.ofModule
deleted def Invertible.copy
deleted def Invertible.mul
deleted def Module.compHom
deleted def Module.IsTorsion'
deleted def Module.IsTorsion
deleted def Module.IsTorsionBy
deleted def Submodule.torsion
deleted def Quandle.Conj
deleted def RingAut
deleted def starMulOfComm
deleted def starRingOfComm
deleted def EuclideanSpace
deleted def NormedField.induced
deleted def NormedRing.induced
deleted def NormedSpace.induced
deleted def ENorm.emetricSpace
deleted def MonoidHom.toFunctor
deleted def Tree.pairwiseNode
deleted def Composition.length
deleted def Quiver.IsThin
deleted def Quiver.Costar
deleted def Quiver.PathStar
deleted def Quiver.Star
deleted def SimpleGraph.induce
deleted def Bifunctor.fst
deleted def Bifunctor.snd
deleted def Bitraversable.tfst
deleted def Bitraversable.tsnd
deleted def Monoid.Foldl
deleted def Monoid.Foldr
deleted def Monoid.foldlM
deleted def Monoid.foldrM
deleted def Functor.mapConstRev
deleted def Cont
deleted def Writer
deleted def ULiftable.down
deleted def ULiftable.up
deleted def Erased.OutType
deleted def Fintype.toOrderBot
deleted def Fintype.toOrderTop
deleted def Matrix.subDown
deleted def Matrix.subDownLeft
deleted def Matrix.subDownRight
deleted def Matrix.subLeft
deleted def Matrix.subRight
deleted def Matrix.subUp
deleted def Matrix.subUpLeft
deleted def Matrix.subUpRight
deleted def Nat.Upto
deleted def Option.iget
deleted def goldenConj
deleted def goldenRatio
deleted def Set.RightInvOn
deleted def Setoid.comap
deleted def Sym2
deleted def Vector3.nth
deleted def Vector3.ofFn
deleted def ZMod.algebra'
deleted def ZMod.algebra
deleted def Units.map'
deleted def Smooth
deleted def SmoothAt
deleted def SmoothOn
deleted def SmoothWithinAt
deleted def SmoothMap
deleted def PointDerivation
deleted def SmoothSection
deleted def TangentBundle
deleted def AddAction.ofEndHom
deleted def DistribSMul.compFun
deleted def MulAction.ofEndHom
deleted def Function.onFun
deleted def Function.swap
deleted def Module.Dual
deleted def ExteriorAlgebra.ι
deleted def ExteriorAlgebra
deleted def FiniteDimensional
deleted def TensorPower
deleted def Function.swap₂
deleted def hidden
deleted def Equiv.Perm.sumCongr
deleted def Equiv.Perm
deleted def Unique.mk'
deleted def Borel
deleted def PadicSeq
deleted def GaussianInt
deleted def LinearOrder.lift'
deleted def LinearOrder.lift
deleted def PartialOrder.lift
deleted def Preorder.lift
deleted def BoundedOrder.lift
deleted def OrderBot.lift
deleted def OrderTop.lift
deleted def IsGreatest.orderTop
deleted def IsLeast.orderBot
deleted def LE.toBtw
deleted def LT.toSBtw
deleted def Complementeds
deleted def GradeOrder.finToNat
deleted def GradeOrder.liftLeft
deleted def Interval
deleted def WellFoundedGT
deleted def WellFoundedLT
deleted def linearOrderOfSTO
deleted def partialOrderOfSO
deleted def Hausdorffification
deleted def IsArtinianRing
deleted def GradedAlgebra
deleted def Ideal
deleted def FractionRing
deleted def multiplicity.Finite
deleted def IsNoetherianRing
deleted def Linarith.Linexp
deleted def Linarith.LinarithM
deleted def Linarith.Monom
deleted def Linarith.Sum
deleted def Bornology.cofinite
deleted def Bornology.induced
deleted def Cube.insertAt
deleted def Cube.splitAt
deleted def GenLoop.cCompInsert
deleted def HomotopyGroup.Pi
deleted def LoopSpace
deleted def Path.Homotopic.proj
deleted def MetricSpace.induced
deleted def Bornology.ofDist
deleted def Scott
deleted def Locale.PT
deleted def UniformSpace.comap
deleted def UniformSpace.ofCore
deleted def UniformSpace.toCore
deleted def Unique.mk'
deleted def S