instRing

Mathlib.Data.Complex.Basic

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

English

There exists a Ring structure on ℂ (the standard one).

Русский

Существует структура кольца на множестве ℂ (стандартная).

LaTeX

$$$\mathbb{C} \text{ carries a ring structure}$$$

Lean4

/-- This shortcut instance ensures we do not find `Ring` via the noncomputable `Complex.field`
instance. -/
instance : Ring ℂ := by infer_instance

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

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

Разделы

Аффилиация

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