Mathlib v3 is deprecated. Go to Mathlib v4

Theorem star_alg_hom.coe_coe

Modification history

2023-03-01 08:55
src/algebra/star/star_alg_hom.lean
fix(algebra/star/star_alg_hom): fix typo in `star_alg_hom.coe_coe` (#18519)
Modified star_alg_hom.coe_coeView on Github →
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 star_alg_hom.coe_coeView on Github →