fact_irreducible_factor — Mathlib

English

Let f be a polynomial over a field K. Then the irreducible factor of f, denoted factor f, is irreducible.

Русский

Пусть f — многочлен над полем K. Тогда неприводимый фактор f, обозначаемый как factor f, является неприводимым.

LaTeX

$$$\\operatorname{Irreducible}(\\operatorname{factor} f)$$$

Lean4

/-- See note [fact non-instances]. -/
theorem fact_irreducible_factor (f : K[X]) : Fact (Irreducible (factor f)) :=
  ⟨irreducible_factor f⟩

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