Commit 2026-06-25 07:54 f8fd74f9

View on Github →

chore: remove unused instances (#41013) Removes unused instances in theorems found by fixing the unused arguments linter to handle theorems in leanprover-community/batteries#1879.

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/Map.lean

modified theorem LinearMap.comap_restrict

Modified Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

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

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

modified theorem IsNonarchimedean.add_eq_max_of_ne'

Modified Mathlib/Algebra/SkewPolynomial/Basic.lean

modified theorem SkewPolynomial.coeff_one_zero

modified theorem SkewPolynomial.monomial_zero_one

Modified Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

modified theorem AlgebraicGeometry.Scheme.Hom.finite_appTop

Modified Mathlib/Analysis/LocallyConvex/HahnBanach.lean

modified theorem Module.Dual.exists_continuous_extension_of_le_seminorm_real

Modified Mathlib/Analysis/Normed/Operator/NormedSpace.lean

modified theorem ContinuousLinearMap.norm_inr

Modified Mathlib/Analysis/Seminorm.lean

modified theorem Seminorm.continuous_finsetSum

Modified Mathlib/CategoryTheory/LiftingProperties/PushoutProduct.lean

modified theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff'

modified theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff

modified theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff'

modified theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

modified theorem IsGaloisGroup.fixedPoints_eq_range_algebraMap

Modified Mathlib/Geometry/Manifold/Algebra/SMul.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean

modified theorem Affine.Simplex.closedInterior_sdiff_interior

modified theorem Affine.Simplex.disjoint_interior_closedInterior_face

modified theorem Affine.Simplex.disjoint_interior_closedInterior_faceOpposite

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

modified theorem measurable_limit_of_tendsto_metrizable_ae

Modified Mathlib/ModelTheory/Satisfiability.lean

modified theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le

Modified Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

Modified Mathlib/Probability/HasCondDistrib.lean

modified theorem ProbabilityTheory.HasLaw.prodMk_of_hasCondDistrib

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/Probability/Independence/Integration.lean

Modified Mathlib/Probability/Independence/Kernel/IndepFun.lean

Modified Mathlib/Probability/Martingale/Centering.lean

modified theorem MeasureTheory.IsPredictable.martingalePart_eq

modified theorem MeasureTheory.IsStronglyPredictable.predictablePart_eq

Modified Mathlib/RingTheory/Ideal/Operations.lean

modified theorem Ideal.inf_ne_bot_of_ne_bot

Modified Mathlib/RingTheory/IsGaloisGroup/Basic.lean

Modified Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean

Modified Mathlib/RingTheory/RamificationInertia/Basic.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean

modified theorem TwoSidedIdeal.finsuppProd_mem

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

modified theorem Submodule.projectionL_eq_self_iff

Modified Mathlib/Topology/Algebra/Order/Floor.lean

modified theorem continuousOn_ceil

Modified Mathlib/Topology/Order/Completion.lean

Modified Mathlib/Topology/Order/ScottTopology.lean

Modified Mathlib/Topology/UniformSpace/ProdApproximation.lean

modified theorem ContinuousMap.denseRange_tensorHom