algebraMap_X

Mathlib.FieldTheory.RatFunc.AsPolynomial

URI: https://scilib.ai/kg/mathlib#RatFunc.algebraMap_X

English

The indeterminate X in K[X] maps to the variable X in RatFunc K under the algebra map.

Русский

Неопределённая переменная X в K[X] переходит в переменную X в RatFunc K через отображение алгебры.

LaTeX

$$$ \mathrm{algebraMap}_{K[X] \to \mathrm{RatFunc} K}(\mathrm{Polynomial.X}) = \mathrm{X} $$$

Lean4

@[simp]
theorem algebraMap_X : algebraMap K[X] (RatFunc K) Polynomial.X = X :=
  rfl

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

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

Разделы

Аффилиация

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