Commit 2025-04-13 01:17 0453a63c

View on Github →

chore: make RingHom.toAlgebra reducible (#23977)

Estimated changes

Modified Mathlib/Algebra/Algebra/Defs.lean

deleted def RingHom.toAlgebra'

deleted def RingHom.toAlgebra

Modified Mathlib/Algebra/Module/RingHom.lean

deleted def RingHom.toModule

Modified Mathlib/RingTheory/Etale/Kaehler.lean