zero_le'

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#zero_le'

English

In a linearly ordered commutative monoid with zero, 0 ≤ a for every a.

Русский

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

LaTeX

$$$0 \le a$$$

Lean4

@[simp]
theorem zero_le' : 0 ≤ a := by simpa only [mul_zero, mul_one] using mul_le_mul_left' (zero_le_one' α) a

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

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

Разделы

Аффилиация

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