isRoot_gcd_iff_isRoot_left_right

Mathlib.Algebra.Polynomial.FieldDivision

URI: https://scilib.ai/kg/mathlib#Polynomial.isRoot_gcd_iff_isRoot_left_right

← MathLib Explorer

English

IsRoot of gcd equals conjunction of IsRoot of each polynomial.

Русский

IsRoot gcd равносильно союзу IsRoot каждого из множеств.

LaTeX

$$IsRoot( gcd f g ) = (IsRoot f ∧ IsRoot g)$$

Lean4

theorem isRoot_gcd_iff_isRoot_left_right [DecidableEq R] {f g : R[X]} {α : R} :
    (EuclideanDomain.gcd f g).IsRoot α ↔ f.IsRoot α ∧ g.IsRoot α :=
  root_gcd_iff_root_left_right

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

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

Разделы

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

Аффилиация

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