zero

Mathlib.Algebra.CubicDiscriminant

URI: https://scilib.ai/kg/mathlib#Cubic.zero

English

For any P, P.toPoly = 0 if and only if P = 0.

Русский

Для любого P: P.toPoly = 0 тогда и только тогда, когда P = 0.

LaTeX

$$$ P.toPoly = 0 \\iff P = 0 $$$

Lean4

theorem zero : (0 : Cubic R).toPoly = 0 :=
  of_d_eq_zero'

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

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

Разделы

Аффилиация

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