eval₂_algebraMap_X — Mathlib

English

For any x, membership in top of Subalgebra equals True.

Русский

Для любого x членство в верху подалгебры равно истине.

LaTeX

$$$x \in \mathrm{top}\; \mathrm{Subalgebra}(R A[X]) \iff \text{True}$$$

Lean4

@[simp]
theorem eval₂_algebraMap_X {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (p : R[X]) (f : R[X] →ₐ[R] A) :
    eval₂ (algebraMap R A) (f X) p = f p :=
  by
  conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]
  simp only [eval₂_eq_sum, sum_def]
  simp only [map_sum, map_mul, map_pow]
  simp [Polynomial.C_eq_algebraMap]
    -- these used to be about `algebraMap ℤ R`, but now the simp-normal form is `Int.castRingHom R`.

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