monic_finprod_X_sub_C

Mathlib.Algebra.Polynomial.Roots

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

English

For any function b from a type to R, the finite product ∏ᶠ (X − C(b k)) is monic.

Русский

Для любой функции b: A → R конечное произведение ∏ᶠ (X − C(b k)) моническое.

LaTeX

$$$\text{Monic}\Big(\prod^{\text{fin}}_{k} (X - C(b(k)))\Big).$$

Lean4

theorem monic_finprod_X_sub_C {α : Type*} (b : α → R) : Monic (∏ᶠ k, (X - C (b k))) :=
  monic_finprod_of_monic _ _ fun a _ => monic_X_sub_C (b a)

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

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

Разделы

Аффилиация

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