Commit 2025-09-03 02:00 477f5971

View on Github →

chore: remove redundant apply invocations (#29188)

Estimated changes

Modified Mathlib/Algebra/Algebra/Spectrum/Basic.lean

Modified Mathlib/Algebra/Algebra/Spectrum/Pi.lean

Modified Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/Lie/Solvable.lean

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Algebra/MvPolynomial/Variables.lean