instStarRing

Mathlib.Algebra.Star.Rat

URI: https://scilib.ai/kg/mathlib#NNRat.instStarRing

English

The nonnegative rationals ℚ≥0 carry a star-ring structure, inherited from commutativity.

Русский

Ненегативные рациональные числа ℚ≥0 обладают структурой звезды-кола, унаследованной от коммутативности.

LaTeX

$$$\\mathrm{StarRing}(\\mathbb{Q}_{\\ge 0}).$$$

Lean4

instance instStarRing : StarRing ℚ≥0 :=
  starRingOfComm

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

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

Разделы

Аффилиация

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