toAddSubgroup

Mathlib.Algebra.Field.Subfield.Defs

URI: https://scilib.ai/kg/mathlib#Subfield.toAddSubgroup

English

The additive part of a subfield forms an additive subgroup of the ambient field.

Русский

Добавление к подполю образует подгруппу сложения в окружающем поле.

LaTeX

$$$\text{toAddSubgroup}(s) = { s.toSubring.toAddSubgroup }$$$

Lean4

/-- The underlying `AddSubgroup` of a subfield. -/
def toAddSubgroup (s : Subfield K) : AddSubgroup K :=
  { s.toSubring.toAddSubgroup with }

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

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

Разделы

Аффилиация

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