eval_apply — Mathlib

English

For q in R and fields R,S with a ring hom f, evaluating cyclotomic after applying f to the input equals applying f to the evaluation of cyclotomic on the original input.

Русский

Для q в R и полей R,S с гомоморфизмом f, применение eval к cyclotomic после применения f к аргументу равно применению f к eval на исходном аргументе.

LaTeX

$$$\operatorname{eval}(f(q), \operatorname{cyclotomic} n S) = f(\operatorname{eval}(q, \operatorname{cyclotomic} n R))$$$

Lean4

theorem eval_apply {R S : Type*} (q : R) (n : ℕ) [Ring R] [Ring S] (f : R →+* S) :
    eval (f q) (cyclotomic n S) = f (eval q (cyclotomic n R)) := by rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]

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