sub_one_lt

Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

English

In a ring with Zero-Le-One structure, −1 < 0 follows from 0 < 1.

Русский

Из 0 < 1 следует, что −1 < 0.

LaTeX

$$$$-1 < 0.$$$$

Lean4

theorem sub_one_lt [ZeroLEOneClass R] [NeZero (1 : R)] [AddLeftStrictMono R] (a : R) : a - 1 < a :=
  sub_lt_iff_lt_add.2 <| lt_add_one a

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

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

Разделы

Аффилиация

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