mapRingHom_id — Mathlib

English

The map that applies the identity ring homomorphism to coefficients is the identity on polynomials.

Русский

Отображение, задающее тождественный гомоморфизм коэффициентов, является тождественным на полиномах.

LaTeX

$$$\\text{mapRingHom}(\\text{RingHom.id }R) = \\text{RingHom.id }(R[X])$$$

Lean4

@[simp]
theorem mapRingHom_id : mapRingHom (RingHom.id R) = RingHom.id R[X] :=
  RingHom.ext fun _x => map_id

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