algebraMap_pi_eq_aeval

Mathlib.RingTheory.Algebraic.Pi

URI: https://scilib.ai/kg/mathlib#Polynomial.algebraMap_pi_eq_aeval

English

For any index i, X_i is transcendental over R in MvPolynomial σ R.

Русский

Для любого индекса i элемент X_i трансцендентален над R в MvPolynomial σ R.

LaTeX

$$$$ \forall i, \ Transcendental R (X_i : MvPolynomial \sigma R). $$$$

Lean4

@[simp]
theorem algebraMap_pi_eq_aeval : (algebraMap R[X] (S → T) : R[X] → S → T) = fun p z => algebraMap _ _ (aeval z p) :=
  rfl

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

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

Разделы

Аффилиация

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