monic_prod_X_sub_C — Mathlib

English

Given a function b from a finite type to R, the product ∏_{a} (X − C(b(a))) over a in the finite set is monic.

Русский

Пусть b: A → R и A конечного типа. Произведение ∏_{a ∈ A} (X − C(b(a))) по a монитическое.

LaTeX

$$$\text{Monic}\Big(\prod_{a \in s} (X - C(b(a)))\Big).$$

Lean4

theorem monic_prod_X_sub_C {α : Type*} (b : α → R) (s : Finset α) : Monic (∏ a ∈ s, (X - C (b a))) :=
  monic_prod_of_monic _ _ fun a _ => monic_X_sub_C (b a)

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