eval_C_X_comp_eval₂_map_C_X — Mathlib

English

In the two-variable polynomial ring R[X][Y], the composition of evaluating in Y at Y and then in X via the canonical algebra maps gives the identity on R[X][Y].

Русский

В кольце полиномов R[X][Y] через две последовательные подстановки (XY-обмен) получаем тождественное отображение на R[X][Y].

LaTeX

$$$\\bigl((\\operatorname{evalRingHom} (\\mathrm{C}X))\\bigr) \\circ (\\operatorname{eval}_{2}(\\operatorname{mapRingHom}(\\mathrm{algebraMap}\\; R\\; R[X][Y]), \\mathrm{C}Y)) = \\mathrm{id}_{R[X][Y]}$$$

Lean4

theorem eval_C_X_comp_eval₂_map_C_X :
    (evalRingHom (C X : R[X][Y])).comp (eval₂RingHom (mapRingHom <| algebraMap R R[X][Y]) (C Y)) = .id _ := by
  ext <;> simp

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