Commit 2025-05-25 19:24 05a2aac1

View on Github →

feat(AlgHom): improve simp normal form (#25177) From Toric

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

added theorem AlgHom.addHomMk_coe

added theorem AlgHom.linearMapMk_toAddHom

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

added theorem NonUnitalAlgHom.addHomMk_coe

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

added theorem LinearMap.mk_coe'

modified theorem LinearMap.mk_coe