instCommGroupSubtypeLtOfNat

Mathlib.Algebra.Order.Positive.Field

URI: https://scilib.ai/kg/mathlib#Positive.instCommGroupSubtypeLtOfNat

English

The positive elements form a commutative group under multiplication.

Русский

Положительные элементы образуют коммутативную группу под действием умножения.

LaTeX

$$$\\{ x\\in K\\; |\\; x>0\\}$ endowed with multiplication is a commutative group.$$

Lean4

instance : CommGroup { x : K // 0 < x } :=
  { Positive.commMonoid with inv_mul_cancel := fun a => Subtype.ext <| inv_mul_cancel₀ a.2.ne' }

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

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

Разделы

Аффилиация

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