Commit 2024-10-21 09:56 59834f40

View on Github →

chore: removed unused variables (#17975) Part of/working towards #17715

Estimated changes

Modified Mathlib/Data/Matrix/Hadamard.lean

Modified Mathlib/Data/Matrix/Reflection.lean

Modified Mathlib/Data/Matroid/Closure.lean

Modified Mathlib/Data/Matroid/IndepAxioms.lean

Modified Mathlib/Data/Matroid/Map.lean

Modified Mathlib/Data/Matroid/Restrict.lean

Modified Mathlib/Data/NNRat/BigOperators.lean

Modified Mathlib/Data/Nat/Factorial/SuperFactorial.lean

Modified Mathlib/Data/Nat/Fib/Zeckendorf.lean

Modified Mathlib/Data/Sum/Interval.lean

Modified Mathlib/Deprecated/Subgroup.lean

Modified Mathlib/Deprecated/Subring.lean

Modified Mathlib/FieldTheory/Finite/Polynomial.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

Modified Mathlib/FieldTheory/IsPerfectClosure.lean

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean

Modified Mathlib/Geometry/Euclidean/PerpBisector.lean

Modified Mathlib/RingTheory/AlgebraicIndependent.lean