mul_unit

Mathlib.FieldTheory.Separable

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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