algebra'' — Mathlib

English

Yet another algebra structure arising from the recursive construction.

Русский

Еще одна алгебраическая структура, возникающая из рекурсивного построения.

LaTeX

$$$\\text{Algebra }K\\; (\\text{SplittingFieldAux}(n.f.removeFactor))$$$

Lean4

instance algebra'' {n : ℕ} {f : K[X]} : Algebra K (SplittingFieldAux n f.removeFactor) :=
  RingHom.toAlgebra (RingHom.comp (algebraMap _ _) (AdjoinRoot.of f.factor))

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