ringHom_eval₂_intCastRingHom — Mathlib

English

Nontrivial (Subalgebra R (Polynomial A)) when A is nontrivial.

Русский

Неоднозначно (Subalgebra R (Polynomial A)) тогда, когда A не тривиальна.

LaTeX

$$$\mathrm{Nontrivial}\; (\mathrm{Subalgebra}\; R\; (\mathrm{Polynomial}\; A))$$$

Lean4

@[simp]
theorem ringHom_eval₂_intCastRingHom {R S : Type*} [Ring R] [Ring S] (p : ℤ[X]) (f : R →+* S) (r : R) :
    f (eval₂ (Int.castRingHom R) r p) = eval₂ (Int.castRingHom S) (f r) p :=
  algHom_eval₂_algebraMap p f.toIntAlgHom r

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