Def NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom

Modification history

2024-09-09 21:54
Mathlib/Algebra/Star/StarAlgHom.lean
refactor: deprecate `StarAlgHomClass` and similar as they just duplicate `StarHomClass` (#16591) …
Modified NonUnitalStarAlgHomClass.toNonUnitalStarAlgHomView on Github →
2023-08-19 12:28
Mathlib/Algebra/Star/StarAlgHom.lean
chore: make sure that some coercions have an attached definition (#6667)
Added NonUnitalStarAlgHomClass.toNonUnitalStarAlgHomView on Github →