ofFractionRing_zero

Mathlib.FieldTheory.RatFunc.Basic

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

English

For any field K, the image of zero in the Fraction Ring of polynomials is the zero element in RatFunc(K).

Русский

Образ нуля в FractionRing полиномиалов является нулём в RatFunc(K).

LaTeX

$$$\operatorname{ofFractionRing}(0) = 0$$$

Lean4

theorem ofFractionRing_zero : (ofFractionRing 0 : RatFunc K) = 0 :=
  zero_def.symm

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

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

Разделы

Аффилиация

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