algebraMap_pi_self_eq_eval

Mathlib.RingTheory.Algebraic.Pi

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

English

For i, f ∈ R[X], Transcendental R (Polynomial.aeval (X_i) f) iff Transcendental R f.

Русский

Для i, f ∈ R[X], Transcendental R (Polynomial.aeval (X_i) f) эквивалентна Transcendental R f.

LaTeX

$$$$ \text{Transcendental } R (Polynomial.aeval (X_i) f) \iff \text{Transcendental } R f. $$$$

Lean4

@[simp]
theorem algebraMap_pi_self_eq_eval : (algebraMap R[X] (R → R) : R[X] → R → R) = fun p z => eval z p :=
  rfl

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

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

Разделы

Аффилиация

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