of_dvd

Mathlib.FieldTheory.Separable

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

Lean4

theorem of_dvd {f g : R[X]} (hf : f.Separable) (hfg : g ∣ f) : g.Separable :=
  by
  rcases hfg with ⟨f', rfl⟩
  exact Separable.of_mul_left hf

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

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

Разделы

Аффилиация

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