Theorem AlgHom.linearMapMk_toAddHom

Modification history

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