ring_hom.of

Stream: general

[Jeremy Avigad]

Whatever happened to ring_hom.of? It used to upgrade a function to a ring_hom.

[Kevin Buzzard]

Did it want an is_ring_hom instance? Those got nuked

[Jeremy Avigad]

Ah. I have eval z : polynomial R -> R. How do I turn it into a ring homomorphism?

[Chris Hughes]

https://leanprover-community.github.io/mathlib_docs/data/polynomial/eval.html#polynomial.eval_ring_hom I think since some changes to the elaborator, we should just make eval a bundled ring hom.

[Yury G. Kudryashov]

@Chris Hughes Last time I tried to turn polynomial.eval into a bundled hom, I got bored by turning all p.eval x to eval x p.

[Yury G. Kudryashov]

Dot notation doesn't work well with this kind of bundled homs.

[Kevin Buzzard]

Will this be any different in Lean 4?

[Kevin Buzzard]

It seems to me that stuff like eval should be "maximally bundled" so the user can forget things later on if they want, rather than having to build up from a bare function.

[Yakov Pechersky]

For eval it might be easy. For things like det it is harder because the proofs about the monoid_homness aren't trivial.