AlgHom, RingHom

Stream: mathlib4

[Kenny Lau]

This is related to #mathlib4 > Simp turning `≠` into `¬ =` and #mathlib4 > AlgHom to RingHom coercion is bad .

Basically, in my journey to formalise the projective space, I've noticed that sometimes I need the AlgHom version of a map, and sometimes I need the RingHom version.

(For example, Spec only takes rings, but AlgHom is more general and easier to construct, e.g. MvPolynomial.aeval.)

And this is another "pain point" for me, since I have to essentially write everything twice. I wonder what the community thinks about this.

[Kenny Lau]

oh, and also this is related to #mathlib4 > simp normal form for symm and coercions

[Peiran Wu]

(deleted)

[Michał Mrugała]

Do you have examples of this pain point? In my experience coercions usually take care of this fine.