HasSeparableContraction — Mathlib

English

There exists a polynomial g such that IsSeparableContraction q f g holds.

Русский

Существует многочлен g, для которого выполняется свойство IsSeparableContraction q f g.

LaTeX

$$$\\mathrm{HasSeparableContraction}_q(f) \\iff \\exists g\\in F[X],\\; \\mathrm{IsSeparableContraction}_q(f,g)$$$

Lean4

/-- The condition of having a separable contraction. -/
def HasSeparableContraction (f : F[X]) : Prop :=
  ∃ g : F[X], IsSeparableContraction q f g

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