aeval_coe

Mathlib.RingTheory.Polynomial.Tower

URI: https://scilib.ai/kg/mathlib#Subalgebra.aeval_coe

English

For a subalgebra S ⊆ A and x ∈ S, aeval x p = aeval x p in A, i.e. evaluation agrees with the ambient algebra.

Русский

Для подалгебры S ⊆ A и x ∈ S выполняется совпадение оценок.

LaTeX

$$$$\\mathrm{aeval}_{x}(p) = \\mathrm{aeval}_{(x:A)}(p)$$$$

Lean4

@[simp]
theorem aeval_coe (S : Subalgebra R A) (x : S) (p : R[X]) : aeval (x : A) p = aeval x p :=
  aeval_algebraMap_apply A x p

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru