algebraMap_eq_C

Mathlib.FieldTheory.RatFunc.AsPolynomial

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

English

The algebra map from rat polynomial ring to RatFunc K coincides with the constant map C.

Русский

Алгебраическое отображение из кольца многочленов в RatFunc совпадает с константным отображением C.

LaTeX

$$algebraMap K[X] (RatFunc K) = C$$

Lean4

@[simp]
theorem algebraMap_eq_C : algebraMap K (RatFunc K) = C :=
  rfl

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

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

Разделы

Аффилиация

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