aeval_map_algebraMap — Mathlib

English

Let R ⊆ A ⊆ B form a tower of algebras. For any p ∈ R[X] and x ∈ B, evaluating after mapping equals mapping after evaluation: aeval x (map (algebraMap R A) p) = map (algebraMap R B) (aeval x p).

Русский

Пусть R ⊆ A ⊆ B образуют башню алгебр. Для любой p ∈ R[X] и x ∈ B выполняется: aeval x (map (algebraMap R A) p) = map (algebraMap R B) (aeval x p).

LaTeX

$$$$\\mathrm{aeval}_x(\\mathrm{map}(\\mathrm{algebraMap}_{R,A})\,p) = \\mathrm{map}(\\mathrm{algebraMap}_{R,B})(\\mathrm{aeval}_x p).$$$$

Lean4

@[simp]
theorem aeval_map_algebraMap (x : B) (p : R[X]) : aeval x (map (algebraMap R A) p) = aeval x p := by
  rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

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