Mathlib Changelog
v4
Changelog
About
Github
Def
StarAlgHomClass.toStarAlgHom
Modification history
2023-08-19 12:28
Mathlib/Algebra/Star/StarAlgHom.lean
chore: make sure that some coercions have an attached definition (#6667)
Added
StarAlgHomClass.toStarAlgHom
View on Github →