[Merged by Bors] - feat: missing results about StarAlgHom.codRestrict

[ADedecker]

This is a step towards making sure that all the codRestrict APIs are similar, but they're still not similar enough in wether they take bundled subobjects/morphisms or subobject/morphism classes.

---

Noticed while reviewing #6372

[eric-wieser]

Suggested change

	theorem coe_codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ x, f x ∈ S) (x : A) :
	theorem codRestrict_apply (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ x, f x ∈ S) (x : A) :

since this mentions x (this also matches LinearMap.codRestrict_apply)

[ADedecker]

I think it's more important that it mirrors AlgHom.coe_codRestrict and NonUnitalStarAlgHom.coe_codRestrict. At some point we want to have a full look at the whole library and make sure that everything is consistent.
I'm going to open issue about that, but I think I prefer to keep this name for now if you think that's okay.

[ADedecker]

#6679

[eric-wieser]

Ah, actually I guess these should be called coe_codRestrict_apply, since the coercion is Subtype.val not just FunLike.coe. But yes, I'm fine leaving the name as is in light of my comment below.

[eric-wieser]

bors d+

[bors]

✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ADedecker]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style