nonneg_toAddGroupCone

Mathlib.Algebra.Order.Ring.Cone

URI: https://scilib.ai/kg/mathlib#RingCone.nonneg_toAddGroupCone

English

The nonnegative cone of T, viewed as a RingCone, equals the nonnegative AddGroupCone on T.

Русский

Неотрицательный конус T, рассматриваемый как RingCone, равен неотрицательному AddGroupCone на T.

LaTeX

$$$ \\text{nonneg } T . \\text{toAddGroupCone} = \\text{AddGroupCone.nonneg } T. $$$

Lean4

@[simp]
theorem nonneg_toAddGroupCone : (nonneg T).toAddGroupCone = .nonneg T :=
  rfl

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

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

Разделы

Аффилиация

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