Def RingHom.toModule
Modification history
2025-04-13 01:17
Mathlib/Algebra/Module/RingHom.lean
chore: make RingHom.toAlgebra reducible (#23977)
Deleted RingHom.toModuleView on Github →2024-11-20 09:38
Mathlib/Algebra/Module/Defs.lean
chore(Algebra/Module): further split `Defs.lean` (#18995) …
Modified RingHom.toModuleView on Github →