Def StarAlgHomClass.toStarAlgHom

Modification history

2026-09-07 13:06
Mathlib/Algebra/Star/StarAlgHom.lean
chore: standardise names for coercions from morphism classes to morphisms (#43367) …
Deleted StarAlgHomClass.toStarAlgHomView on Github →
2023-08-19 12:28
Mathlib/Algebra/Star/StarAlgHom.lean
chore: make sure that some coercions have an attached definition (#6667)
Added StarAlgHomClass.toStarAlgHomView on Github →