Theorem NonUnitalAlgHom.addHomMk_coe

Modification history

2025-05-25 19:24
Mathlib/Algebra/Algebra/NonUnitalHom.lean
feat(AlgHom): improve simp normal form (#25177) …
Added NonUnitalAlgHom.addHomMk_coeView on Github →