toPoly_injective

Mathlib.Algebra.CubicDiscriminant

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

← MathLib Explorer

English

For any cubics P and Q, P.toPoly = Q.toPoly if and only if P = Q.

Русский

Для любых кубических P и Q верно: P.toPoly = Q.toPoly тогда и только тогда, когда P = Q.

LaTeX

$$$ P.toPoly = Q.toPoly \\Leftrightarrow P = Q $$$

Lean4

theorem toPoly_injective (P Q : Cubic R) : P.toPoly = Q.toPoly ↔ P = Q :=
  ⟨fun h ↦ Cubic.ext (a_of_eq h) (b_of_eq h) (c_of_eq h) (d_of_eq h), congr_arg toPoly⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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