of_mul_right

Mathlib.FieldTheory.Separable

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

English

If the product f g is separable, then g is separable.

Русский

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

LaTeX

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

Lean4

theorem of_mul_right {f g : R[X]} (h : (f * g).Separable) : g.Separable :=
  by
  rw [mul_comm] at h
  exact h.of_mul_left

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

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

Разделы

Аффилиация

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