splits_iff — Mathlib

English

For polynomials over a field, Splits i f holds iff f = 0 or every irreducible g dividing f.map i has degree 1.

Русский

Для многочленов над полем, Splits i f эквивалентно либо f = 0, либо для любого ирредуцируемого g, делящего f.map i, deg g = 1.

LaTeX

$$$\operatorname{Splits}_i(f) \iff \left(f = 0 \lor \forall g:\text{L[X]}, \operatorname{Irreducible}(g) \to g \mid f.map i \to \deg g = 1\right)$$$

Lean4

/-- This lemma is for polynomials over a field. -/
theorem splits_iff (f : K[X]) : Splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1 := by
  rw [Splits, Polynomial.map_eq_zero]

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