coe_fn

Stream: general

[Yury G. Kudryashov]

Making polynomial.C a bundled homomorphism had almost no side effects, thanks a lot @Gabriel Ebner !

The old code (or a substitution code I tried) failed in a few places:

• one can't write C_neg [comm_ring α] (a : α) : C (-a) = -C a := C.map_neg a because by the time Lean parses C.map_neg it doesn't know yet that the base type is a ring, not only a semiring. Both (C : α →ₐ[α] _).map_neg a and alg_hom.map_neg _ a work. Similarly for other dot notation.
• congr failed to go from C a = 1 to a = 1. I think that convert C_1 better describes what we want Lean to do.
• C 1 is a polynomial nat, not polynomial ?m_1.

[Johan Commelin]

This is nice.

[Johan Commelin]

On the witt-vectors2 branch, I also worked a lot with C_hom, map_hom, rename_hom, and eval2_hom, all for mv_polynomial. It seems to work really well.

[Johan Commelin]

But I didn't yet integrate it into the library.