polynomial `eval_ring_hom` and `eval_linear_map`

Stream: Is there code for X?

[Kevin Buzzard]

import data.polynomial.eval

variables (R : Type*) [comm_semiring R]

namespace polynomial

noncomputable def eval_ring_hom (x : R) : polynomial R →+* R :=
{ to_fun := eval x,
  map_zero' := eval_zero,
  map_add' := λ _ _, eval_add,
  map_one' := eval_one,
  map_mul' := λ _ _, eval_mul, }

noncomputable def evalₗ (x : R) : polynomial R →ₗ[R] R :=
{ to_fun := eval x,
  map_add' := λ _ _, eval_add,
  map_smul' := λ r f, eval_smul f x }

end polynomial

Are these missing?

[Bhavik Mehta]

Aren't they eval₂_ring_hom (ring_hom.id R)?

[Adam Topaz]

Or even docs#polynomial.aeval

[Adam Topaz]

Maybe with a .to_ring_hom

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

aargh data.polynomial.algebra_map isn't imported by algebra.polynomial.group_ring_action (where I need this)