algebra''' — Mathlib

English

There is an algebra structure on SplittingFieldAux(n,f.removeFactor) obtained via the previous construction.

Русский

Существует структура алгебры на SplittingFieldAux(n,f.removeFactor), полученная предыдущей конструкцией.

LaTeX

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

Lean4

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

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