Commit 2024-05-17 19:31 cec63ac9

View on Github →

style: remove all isolated where (#12991)

Estimated changes

modified def NonUnitalAlgHom.prod
modified def Submodule.mapHom
modified def Subalgebra.inclusion
modified def Finsupp.liftAddHom
modified def ringEquivIsoRingIso
modified def DirectSum.mk
modified def DirectSum.sigmaCurry
modified def FreeMonoid.map
modified def Submodule.negOrderIso
modified def Polynomial.revAt
modified def Quandle.Conj.map
modified def Rack.selfApplyEquiv
modified def Rack.toConj
modified def Rack.toEnvelGroup
modified def ShelfHom.comp
modified def StarAlgHom.prodEquiv
modified def unitary.toUnits
modified def Submonoid.unitSphere
modified def Subsemigroup.unitBall
modified def GroupSeminorm.comp
modified def equivIsoIso
modified def compositionAsSetEquiv
modified def compositionEquiv
modified def hallMatchingsFunctor
modified def Prefunctor.symmetrify
modified def DFA.toNFA
modified def Traversable.mapFold
modified def DFinsupp.eraseAddHom
modified def DFinsupp.liftAddHom
modified def DFinsupp.singleAddHom
modified def FinEnum.ofEquiv
modified def Finset.symInsertEquiv
modified def Finsupp.comapDomain
modified def Finsupp.filterAddHom
modified def Finsupp.splitComp
modified def Finsupp.subtypeDomain
modified def Finsupp.single
modified def Finsupp.indicator
modified def unitsEquivProdSubtype
modified def Multiset.coeEmbedding
modified def Multiset.coeEquiv
modified def SetSemiring.imageHom
modified def Sym2.lift
modified def Sym2.sym2EquivSym'
modified def WType.equivSigma
modified def WType.equivList
modified def MonoidHom.of
modified def Subgroup.of
modified def RatFunc.map
modified def Con.correspondence
modified def Con.lift
modified def Con.mulKer
modified def Con.ofSubmonoid
modified def fixingSubmonoid
modified def MulActionHom.ofEq
modified def LinearMap.lflip
modified def CliffordAlgebra.lift
modified def Finsupp.lcomapDomain
modified def Finsupp.lmapDomain
modified def MultilinearMap.map
modified def MultilinearMap.prod
modified def LinearMap.graph
modified structure QuadraticForm
modified def Submodule.mapQLinear
modified def Fin.castLEOrderIso
modified def OrderIso.piFinTwoIso
modified def finProdFinEquiv
modified def finSuccEquiv'
modified def finSumFinEquiv
modified def piFinTwoEquiv
modified def ModularForm.mcast
modified def ClosureOperator.mk₂
modified def Filter.comap
modified def Heyting.Regular.gi
modified def Equiv.toOrderIsoSet
modified def sInfHom.comp
modified def sSupHom.comp
modified def sSupHom.setImage
modified def Finpartition.bind
modified def Finpartition.copy
modified def Finpartition.extend
modified def upperSetIsoLowerSet
modified def algHomEquivSigma
modified def RingCon.mk'
modified def Ideal.idealProdEquiv
modified def GenLoop.loopHomeo
modified def GenLoop.toLoop
modified def UniformEquiv.image
modified def UniformEquiv.piFinTwo
modified def UniformEquiv.prodComm
modified def UniformEquiv.setCongr