instAlgebra — Mathlib

English

There is an Algebra R (AlgebraicClosure k) structure, i.e., AlgebraicClosure k is an algebra over any commutative semiring R with an algebra structure on k mapping to it.

Русский

Существует структура Algebra R (AlgebraicClosure k), то есть AlgebraicClosure k является R-алгеброй.

LaTeX

$$$\text{Algebra } R (\text{AlgebraicClosure}(k)).$$$

Lean4

instance instAlgebra {R : Type*} [CommSemiring R] [Algebra R k] : Algebra R (AlgebraicClosure k) :=
  Ideal.Quotient.algebra _

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