Commit 2026-04-19 00:33 f3dd886f

View on Github →

chore: adaptations for overlapping instances linter (#38151) This PR contains adaptations for the overlapping instances linter (#38126)

Estimated changes

Modified Mathlib/Algebra/Algebra/Shrink.lean

modified def Shrink.algEquiv

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean

Modified Mathlib/Algebra/Homology/HomologySequence.lean

Modified Mathlib/Algebra/Module/Lattice.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

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

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

modified def WeierstrassCurve.Affine.Point.add

Modified Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

modified theorem AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app

modified theorem AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app

modified def AlgebraicGeometry.Scheme.Modules.restrictFunctor

modified def AlgebraicGeometry.Scheme.Modules.restrictFunctorComp

modified theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app

modified theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app

modified def AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso

Modified Mathlib/AlgebraicTopology/ModelCategory/IsCofibrant.lean

Modified Mathlib/Analysis/Distribution/DerivNotation.lean

Modified Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

Modified Mathlib/Analysis/InnerProductSpace/Harmonic/HarmonicContOnCl.lean

modified theorem InnerProductSpace.HarmonicContOnCl.continuousOn_ball

Modified Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean

Modified Mathlib/Analysis/Normed/Ring/WithAbs.lean

modified def WithAbs.linearEquiv

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

modified def spectralNorm.nontriviallyNormedField

Modified Mathlib/CategoryTheory/Adhesive/Subobject.lean

Modified Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean

Modified Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

modified def CategoryTheory.GrpObj.ofInvertible

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

Modified Mathlib/CategoryTheory/Shift/Adjunction.lean

Modified Mathlib/CategoryTheory/Shift/Pullback.lean

modified def CategoryTheory.PullbackShift

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

modified def CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility

Modified Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean

Modified Mathlib/CategoryTheory/Sites/Hypercover/One.lean

Modified Mathlib/CategoryTheory/Sites/Point/OfIsCofiltered.lean

Modified Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean

Modified Mathlib/CategoryTheory/Sites/Pullback.lean

modified def CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuous

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean

Modified Mathlib/Combinatorics/Matroid/Rank/Cardinal.lean

Modified Mathlib/Data/Finset/SMulAntidiagonal.lean

Modified Mathlib/FieldTheory/Finite/Extension.lean

modified def FiniteField.Extension

Modified Mathlib/FieldTheory/PurelyInseparable/Exponent.lean

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

Modified Mathlib/NumberTheory/NumberField/Units/Basic.lean

modified def NumberField.Units.torsionOrder

Modified Mathlib/Order/CompleteLattice/PiLex.lean

Modified Mathlib/Order/CompletePartialOrder.lean

Modified Mathlib/Order/MinMax.lean

Modified Mathlib/Probability/Independence/Process/HasIndepIncrements/IsGaussianProcess.lean

Modified Mathlib/RepresentationTheory/Rep/Res.lean

Modified Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

Modified Mathlib/RingTheory/Algebraic/Integral.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean

Modified Mathlib/RingTheory/Extension/Presentation/Submersive.lean

modified theorem Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply

Modified Mathlib/RingTheory/GradedAlgebra/Basic.lean

Modified Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

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

Modified Mathlib/RingTheory/Localization/AtPrime/Extension.lean

Modified Mathlib/RingTheory/Morita/Matrix.lean

Modified Mathlib/RingTheory/MvPowerSeries/Rename.lean

modified def MvPowerSeries.rename

modified def MvPowerSeries.renameFun

Modified Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

Modified Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean

modified theorem Algebra.SubmersivePresentation.cotangentComplexAux_injective

modified theorem Algebra.SubmersivePresentation.cotangentComplexAux_surjective

modified theorem Algebra.SubmersivePresentation.sectionCotangent_eq_iff

Modified Mathlib/Tactic/Translate/Reorder.lean

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

Modified Mathlib/Topology/Algebra/Module/Spaces/PointwiseConvergenceCLM.lean

modified def PointwiseConvergenceCLM.precomp

Modified Mathlib/Topology/Algebra/Valued/WithVal.lean

Modified Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean

Modified Mathlib/Topology/Convenient/GeneratedBy.lean

modified def Topology.IsGeneratedBy.homeomorph

Modified Mathlib/Topology/Sion.lean

modified def Sion.setOf_sublevelLeft_subset

Modified Mathlib/Topology/VectorBundle/Basic.lean