IsSeparableContraction — Mathlib

English

A separable contraction of a polynomial f ∈ F[X] is a separable polynomial g ∈ F[X] together with an m ∈ ℕ such that expand F (q^m) g = f.

Русский

Разделимая конракция многочлена f ∈ F[X] — это разделимый многочлен g ∈ F[X] и целое m ≥ 0 такое, что expand F (q^m) g = f.

LaTeX

$$$\\forall f,g \\in F[X],\\; \\mathrm{IsSeparableContraction}_q(f,g) \\iff g\\text{ Separable} \\wedge \\exists m\\in\\mathbb{N},\\; \\mathrm{expand}\\ F (q^m)\\ g = f$$$

Lean4

/-- A separable contraction of a polynomial `f` is a separable polynomial `g` such that
`g(x^(q^m)) = f(x)` for some `m : ℕ`. -/
def IsSeparableContraction (f : F[X]) (g : F[X]) : Prop :=
  g.Separable ∧ ∃ m : ℕ, expand F (q ^ m) g = f

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