Commit 2025-07-22 17:58 5fe840bb

View on Github →

chore(*): review the nolints for unusedVariables (#27350) This was initially intended to review adaptation notes for lean4#5338, but it turns out a lot of previous unused variables lints are already silent. So we can remove a lot of them.

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

Modified Mathlib/Algebra/DualNumber.lean

modified theorem DualNumber.lift_apply_inl

modified theorem DualNumber.lift_comp_inlHom

modified theorem DualNumber.lift_op_smul

modified theorem DualNumber.lift_smul

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

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/Data/FP/Basic.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/Nat/Log.lean

Modified Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

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

Modified Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

Modified Mathlib/RingTheory/Regular/RegularSequence.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/Tactic/Explode.lean

Modified Mathlib/Tactic/Order/CollectFacts.lean

Modified Mathlib/Topology/ApproximateUnit.lean

Modified Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean