algebraMap_succ — Mathlib

English

The algebra map at the successor stage satisfies a compatibility with the previous stage via the X-operator.

Русский

Алгебраическое отображение на следующем этапе совместимо с предыдущим через оператор X.

LaTeX

$$$\\text{algebraMap }K\\; (\\text{SplittingFieldAux}(n+1,f)) = (\\text{algebraMap }(\\operatorname{AdjoinRoot} f.factor) (\\text{SplittingFieldAux} n f.removeFactor)).\\text{comp} (\\operatorname{AdjoinRoot.of } f.factor)$$$

Lean4

theorem algebraMap_succ (n : ℕ) (f : K[X]) :
    algebraMap K (SplittingFieldAux (n + 1) f) =
      (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor) :=
  rfl

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