C

Mathlib.FieldTheory.RatFunc.AsPolynomial

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

English

In the RatFunc construction, C is the constant rational function

Русский

В конструкции RatFunc C — константная рациональная функция

LaTeX

$$C : K →+* RatFunc K$$

Lean4

/-- `RatFunc.C a` is the constant rational function `a`. -/
def C : K →+* RatFunc K :=
  algebraMap _ _

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

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

Разделы

Аффилиация

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