instStarRingNNReal

Mathlib.Data.NNReal.Star

URI: https://scilib.ai/kg/mathlib#instStarRingNNReal

English

The nonnegative reals form a star ring under the canonical star operation (trivial star).

Русский

Обобщение ℝ≥0 образует звездообразную кольцевую структуру с тривиальным звёздчатым отображением.

LaTeX

$$$ \text{ NNReal is a StarRing under the trivial star. }$$$

Lean4

instance : StarRing ℝ≥0 :=
  starRingOfComm

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

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

Разделы

Аффилиация

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