Commit 2024-09-30 00:42 9f502c28

View on Github →

chore: remove some unused variables (#17261) Inspired by #17178 and found by a linter.

Estimated changes

Modified Mathlib/Algebra/Field/Basic.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

Modified Mathlib/Algebra/Group/Semiconj/Units.lean

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Commute.lean

Modified Mathlib/Algebra/GroupWithZero/InjSurj.lean

Modified Mathlib/Algebra/GroupWithZero/Semiconj.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

Modified Mathlib/Algebra/Module/BigOperators.lean

Modified Mathlib/Algebra/Polynomial/Induction.lean

Modified Mathlib/Algebra/Ring/Basic.lean

Modified Mathlib/Algebra/Ring/Commute.lean

Modified Mathlib/Algebra/Ring/Hom/Defs.lean

Modified Mathlib/Algebra/Ring/Semiconj.lean

Modified Mathlib/Algebra/Ring/Units.lean

Modified Mathlib/Control/Basic.lean

Modified Mathlib/Control/Lawful.lean

Modified Mathlib/Data/Subtype.lean

Modified Mathlib/Lean/PrettyPrinter/Delaborator.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Function/Conjugate.lean

Modified Mathlib/Logic/Relator.lean

Modified Mathlib/Logic/Unique.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/Defs.lean

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

Modified Mathlib/Order/Max.lean

Modified Mathlib/Order/SuccPred/Basic.lean

Modified Mathlib/Probability/Kernel/Disintegration/Integral.lean

Modified Mathlib/Topology/AlexandrovDiscrete.lean

Modified Mathlib/Topology/MetricSpace/Infsep.lean

Modified Mathlib/Topology/MetricSpace/ShrinkingLemma.lean