map_intCast — Mathlib

English

Let f: R →+* S be a ring homomorphism. For every integer n, the map of the constant polynomial ↑n is the constant polynomial ↑n in S[X].

Русский

Пусть f: R →+* S — кольцевое отображение. Для каждого целого числа n отображение константного полинома ↑n по f даёт константный полином ↑n в S[X].

LaTeX

$$$Polynomial.map\\ f\\ (↑n) = ↑n$$$

Lean4

@[simp]
protected theorem map_intCast {S} [Ring S] (f : R →+* S) (n : ℤ) : map f ↑n = ↑n :=
  map_intCast (mapRingHom f) n

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