Commit 2025-11-14 05:35 ef549b7b

View on Github →

chore: add grind annotations for homomorphisms (#29576)

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/FreeAlgebra.lean

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

Modified Mathlib/Algebra/Homology/Homotopy.lean

Modified Mathlib/Algebra/Lie/BaseChange.lean

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

Modified Mathlib/Algebra/Polynomial/RuleOfSigns.lean