instDivInvMonoid

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.instDivInvMonoid

English

The complex numbers carry a division-inverse monoid structure (i.e., a division ring).

Русский

Комплексные числа образуют дивизионное кольцо (деление существует для ненулевых элементов).

LaTeX

$$$$\mathbb{C} \text{ has a division-inverse monoid structure.}$$$$

Lean4

noncomputable instance instDivInvMonoid : DivInvMonoid ℂ where

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

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

Разделы

Аффилиация

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