exists_irreducible_of_natDegree_ne_zero

Mathlib.RingTheory.Polynomial.UniqueFactorization

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

← MathLib Explorer

English

If natDegree f ≠ 0, then there exists an irreducible g with g ∣ f.

Русский

Если natDegree f ≠ 0, существует ирред. g с g|f.

LaTeX

$$$$\\operatorname{natDegree}(f) \\neq 0 \\Rightarrow \\exists g\\; (\\text{Irreducible } g \\land g \\mid f).$$$$

Lean4

theorem exists_irreducible_of_natDegree_ne_zero (hf : f.natDegree ≠ 0) : ∃ g, Irreducible g ∧ g ∣ f :=
  exists_irreducible_of_natDegree_pos <| Nat.pos_of_ne_zero hf

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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