zero_tsub

Mathlib.Algebra.Order.Sub.Basic

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

English

In a canonically ordered additive structure, 0 − a = 0 for all a.

Русский

В канонически упорядоченной аддитивной структуре 0 − a = 0 для всех a.

LaTeX

$$$$ 0 - a = 0 $$$$

Lean4

@[simp]
theorem zero_tsub (a : α) : 0 - a = 0 :=
  tsub_eq_zero_of_le <| zero_le a

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

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

Разделы

Аффилиация

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