ofMul_le

Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags

URI: https://scilib.ai/kg/mathlib#Additive.ofMul_le

English

The embedding of α into Additive α via ofMul preserves order: ofMul a ≤ ofMul b iff a ≤ b.

Русский

Встраивание α в Additive α через ofMul сохраняет порядок: ofMul a ≤ ofMul b ⇔ a ≤ b.

LaTeX

$$$\operatorname{ofMul} a \le \operatorname{ofMul} b \iff a \le b$$$

Lean4

@[simp]
theorem ofMul_le {a b : α} : ofMul a ≤ ofMul b ↔ a ≤ b :=
  Iff.rfl

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

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

Разделы

Аффилиация

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