instCommRing

Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

URI: https://scilib.ai/kg/mathlib#AlgebraicClosure.instCommRing

English

The algebraic closure AlgebraicClosure(k) carries a natural commutative ring structure.

Русский

У замыкания AlgebraicClosure(k) естественная коммутативная кольцевая структура.

LaTeX

$$$\text{CommRing}(\text{AlgebraicClosure}(k)).$$$

Lean4

instance instCommRing : CommRing (AlgebraicClosure k) :=
  Ideal.Quotient.commRing _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru