Splits — Mathlib

English

A polynomial Splits after a ring hom K → L if either its map is zero or all irreducible factors have degree 1.

Русский

Полином раскладывается после кольцеобразного отображения, либо его образ равен нулю, либо все неприводимые множители имеют степень 1.

LaTeX

$$Splits i f := (f.map i = 0) ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1$$

Lean4

/-- A polynomial `Splits` iff it is zero or all of its irreducible factors have `degree` 1. -/
def Splits (f : K[X]) : Prop :=
  f.map i = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1

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