removeFactor — Mathlib

English

Defines a quotient to remove one factor of a polynomial in an extended field where a root lies; it formalizes the division step used in constructing a splitting field.

Русский

Определяет операцию удаления одного множителя многочлена в расширенном поле, где лежит корень; описывает шаг деления при построении разворачивающего поля.

LaTeX

$$$\\text{removeFactor}(f) : \\text{Polynomial}(\\text{AdjoinRoot }f\\!\\text{.factor})$$$

Lean4

/-- Divide a polynomial f by `X - C r` where `r` is a root of `f` in a bigger field extension. -/
def removeFactor (f : K[X]) : Polynomial (AdjoinRoot <| factor f) :=
  map (AdjoinRoot.of f.factor) f /ₘ (X - C (AdjoinRoot.root f.factor))

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