root_or_root_of_root_mul

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

A ring homomorphism f preserves products, so map of a product equals product of maps: f(∏ p_i) = ∏ f(p_i).

Русский

Гомоморфизм f сохраняет произведения: f(∏ p_i) = ∏ f(p_i).

LaTeX

$$$f\\left(\\prod_{i} p_i\\right) = \\prod_{i} f(p_i)$$$

Lean4

theorem root_or_root_of_root_mul (h : IsRoot (p * q) a) : IsRoot p a ∨ IsRoot q a :=
  root_mul.1 h

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

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

Разделы

Аффилиация

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