Commit 2026-10-28 01:55 04a3376c

View on Github →

chore: fix mergewithgrind exceptions (#45037) This fixes the warnings from the mergeWithGrind linter, as reported [here](#mathlib4 > Weekly linting log @ 💬) by @SnirBroshi. Some files become a bit slower, see radar output below, but nothing significant IMO.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Variables.lean

Modified Mathlib/Algebra/Notation/Support.lean

Modified Mathlib/Algebra/QuadraticAlgebra/Discriminant.lean

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/ToMkOne.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

Modified Mathlib/Analysis/Calculus/Taylor.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

Modified Mathlib/Combinatorics/SimpleGraph/Tutte.lean

Modified Mathlib/Data/Finsupp/Pointwise.lean

Modified Mathlib/Data/List/Nodup.lean

modified theorem List.nodup_iff_count_eq_one

Modified Mathlib/Data/Multiset/Find.lean

Modified Mathlib/Data/PFun.lean

Modified Mathlib/Geometry/Manifold/Instances/Real.lean

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

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/MeasureTheory/VectorMeasure/IntegrationByParts.lean

Modified Mathlib/NumberTheory/FundamentalDiscriminant.lean

Modified Mathlib/NumberTheory/Height/EllipticCurve.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/Order/Interval/Finset/Gaps.lean

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean