Commit 2025-07-15 12:22 e87547a2

View on Github →

chore: golf Algebra/ using simp/simp_all (#27130)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Azumaya/Basic.lean

Modified Mathlib/Algebra/BigOperators/Sym.lean

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

Modified Mathlib/Algebra/Lie/Semisimple/Basic.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

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

Modified Mathlib/Algebra/Module/Presentation/Differentials.lean

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

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

Modified Mathlib/Algebra/Order/Group/Indicator.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

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

Modified Mathlib/Algebra/Polynomial/Derivative.lean

Modified Mathlib/Algebra/Polynomial/Eval/Coeff.lean

Modified Mathlib/Algebra/Polynomial/GroupRingAction.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/Algebra/Prime/Lemmas.lean

Modified Mathlib/Algebra/Ring/Rat.lean