Mathlib v3 is deprecated. Go to Mathlib v4

Theorem non_unital_star_alg_hom.coe_coe

Modification history

2022-11-10 15:12
src/algebra/star/star_alg_hom.lean
feat(algebra/*): add coercions from hom classes to their respective homs (#17000) …
Added non_unital_star_alg_hom.coe_coeView on Github →