Commit 2026-06-16 09:46 d292472f

View on Github →

feat: expand API for StarAlgEquiv (#40517) This PR adds API for StarAlgEquiv. It provides:

  • StarAlgEquiv.toNonUnitalStarAlgHom
  • StarAlgEquiv.toStarAlgHom
  • StarAlgEquiv.arrowCongr' (non-unital morphisms)
  • StarAlgEquiv.arrowCongr (unital morphisms)
  • StarAlgEquiv.ofNonUnitalStarAlgHom (non-unital morphisms)
  • StarAlgEquiv.ofStarAlgHom (unital morphisms); this was pre-existing, but used morphism classes instead of actual morphisms. This PR fixes that. It also generalizes the type class hypothesis in StarAlgEquiv.restrictScalars so that it applies to non-unital algebras. In addition, StarAlgEquiv.refl is protected and its type arguments made explicit.

Estimated changes

modified theorem StarAlgEquiv.coe_refl
deleted def StarAlgEquiv.refl
modified theorem StarAlgEquiv.refl_symm