eval₂Hom_comp_C — Mathlib

English

Let f be a ring homomorphism and g a coefficient map; evaluating constant polynomials under eval₂Hom recovers f.

Русский

Пусть f — гомоморфизм и g — отображение коэффициентов; преобразование констант через eval₂Hom возвращает f.

LaTeX

$$$$ (\mathrm{eval}_2\mathrm{Hom}\, f\, g) \circ \mathrm{C} = f $$$$

Lean4

@[simp]
theorem eval₂Hom_comp_C (f : R →+* S) (g : σ → S) : (eval₂Hom f g).comp C = f :=
  by
  ext1 r
  exact eval₂_C f g r

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