aevalTower_comp_C — Mathlib

English

Composing aevalTower with the constant polynomial embedding C recovers the original map g: (aevalTower g y) ∘ C = g.

Русский

Составление aevalTower с константным вложением C восстанавливает исходное отображение: (aevalTower g y) ∘ C = g.

LaTeX

$$(aevalTower g y) ∘ C = g$$

Lean4

@[simp]
theorem aevalTower_comp_C : (aevalTower g y : R[X] →+* A').comp C = g :=
  RingHom.ext <| aevalTower_C _ _

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