instGroupWithZero

Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

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

English

The algebraic closure AlgebraicClosure(k) forms a group with zero under multiplication, i.e., a GroupWithZero.

Русский

Алгебраическое замыкание AlgebraicClosure(k) образует группу с нулём по умножению.

LaTeX

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

Lean4

instance instGroupWithZero : GroupWithZero (AlgebraicClosure k) where __ := Ideal.Quotient.field _

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

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

Разделы

Аффилиация

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