unit_mul

Mathlib.FieldTheory.Separable

URI: https://scilib.ai/kg/mathlib#Polynomial.Separable.unit_mul

English

If f is a unit and g is separable, then f g is separable.

Русский

Если f — единица и g разделим, то f g разделим.

LaTeX

$$$\\operatorname{IsUnit}(f) \\Rightarrow \\operatorname{Separable}(g) \\Rightarrow \\operatorname{Separable}(f g)$$$

Lean4

theorem unit_mul {f g : R[X]} (hf : IsUnit f) (hg : g.Separable) : (f * g).Separable :=
  (associated_unit_mul_right g f hf).separable hg

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

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

Разделы

Аффилиация

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