eval₂_at_apply — Mathlib

English

Let f : R →+* S be a ring homomorphism and r ∈ R. Then p.eval₂ f (f r) = f (p.eval r) for any p ∈ R[X].

Русский

Пусть f : R →+* S — гомоморфизм колец и r ∈ R. Тогда для любого p ∈ R[X] выполняется p.eval₂ f (f r) = f (p.eval r).

LaTeX

$$$ p.\mathrm{eval}_2 f (f r) = f (p.\mathrm{eval} r) $$$

Lean4

@[simp]
theorem eval₂_at_apply {S : Type*} [Semiring S] (f : R →+* S) (r : R) : p.eval₂ f (f r) = f (p.eval r) :=
  by
  rw [eval₂_eq_sum, eval_eq_sum, sum, sum, map_sum f]
  simp only [f.map_mul, f.map_pow]

Похожие утверждения