feat(Algebra/Star/StarRingHom): Add non-unital star ring homomorphisms

[mans0954]

trafficstars

Definitions and basic properties of non-unital star ring homomorphisms

---

[j-loreaux]

no need to include me in the copyright.

[mans0954]

Looks like a decent start, but still a lot of the API is missing. It's okay if you add it in follow-up PRs though.

I've fleshed out the API now.

Also, when you're done with this, would you mind fixing up StarRingHomClass.instOrderHomClass and StarRingHomClass.instOrderIsoClass to use these new classes (and renaming the latter?

I've done this in a separate PR #13089.

[github-actions[bot]]

Import summary

No significant changes to the import graph

[github-actions[bot]]

PR summary 822b578d5d

Import changes

No significant changes to the import graph

---

Declarations diff

+ NonUnitalStarRingHom + NonUnitalStarRingHomClass + Simps.symm_apply + StarRingEquiv + StarRingEquivClass + apply_symm_apply + coe_coe + coe_comp + coe_copy + coe_id + coe_ofBijective + coe_one + coe_refl + coe_toNonUnitalRingHom + coe_trans + coe_zero + comp + comp_apply + comp_assoc + comp_id + copy + copy_eq + ext_iff + id + id_comp + instCoeHead + instance (priority := 100) {F A B : Type*} [NonUnitalNonAssocSemiring A] [Star A] + instance (priority := 50) {F A B : Type*} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B] + instance : EquivLike (A ≃⋆+* B) A B + instance : FunLike (A →⋆ₙ+* B) A B + instance : FunLike (A ≃⋆+* B) A B + instance : Inhabited (A →⋆ₙ+* B) + instance : Inhabited (A ≃⋆+* A) + instance : Monoid (A →⋆ₙ+* A) + instance : MonoidWithZero (A →⋆ₙ+* A) + instance : NonUnitalRingHomClass (A →⋆ₙ+* B) A B + instance : NonUnitalStarRingHomClass (A →⋆ₙ+* B) A B + instance : RingEquivClass (A ≃⋆+* B) A B + instance : StarRingEquivClass (A ≃⋆+* B) A B + instance : Zero (A →⋆ₙ+* B) + instance [NonUnitalStarAlgHomClass F R A B] : NonUnitalStarRingHomClass F A B + instance [NonUnitalStarRingHomClass F A B] : CoeHead F (A →⋆ₙ+* B) + invFun_eq_symm + leftInverse_symm + ofBijective + ofBijective_apply + ofStarRingHom + one_apply + refl + refl_symm + rightInverse_symm + symm + symm_apply_apply + symm_bijective + symm_mk + symm_mk.aux + symm_symm + symm_trans_apply + toNonUnitalStarRingHom + toRingEquiv_eq_coe + toStarRingEquiv + trans + trans_apply + zero_apply ++ Simps.apply ++ coe_mk ++ ext ++ mk_coe

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[j-loreaux]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style