Commit 2024-06-24 21:15 04fc89bc

View on Github →

refactor(Algebra/Star/StarAlgHom): mk_coe and coe_mk in StarAlgHom (#13267) Add mk_coe and coe_mk results to Algebra/Star/StarAlgHom in analogy with RingEquiv.

Estimated changes

added theorem StarAlgEquiv.coe_mk
deleted theorem StarAlgEquiv.mk_coe'
added theorem StarAlgEquiv.mk_coe