Commit 2025-07-22 21:03 a2ebfe17

View on Github →

chore: use simp or simp_all instead of aesop in Algebra/ (#27266) Motivation: reducing overhead and clarifying intent.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/BigOperators/Group/List/Basic.lean

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

modified theorem Finset.empty_zpow

Modified Mathlib/Algebra/GroupWithZero/Associated.lean

Modified Mathlib/Algebra/Lie/TraceForm.lean

Modified Mathlib/Algebra/Module/CharacterModule.lean

Modified Mathlib/Algebra/Module/Submodule/Range.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Order/Antidiag/Nat.lean

Modified Mathlib/Algebra/Order/Antidiag/Pi.lean

Modified Mathlib/Algebra/Order/Ring/Star.lean

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Modified Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

Modified Mathlib/Algebra/Polynomial/Degree/Monomial.lean

Modified Mathlib/Algebra/Polynomial/SpecificDegree.lean