ofMul_lt

Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags

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

English

The embedding Additive α → Multiplicative α preserves strict order: ofAdd a < ofAdd b iff a < b.

Русский

Встраивание Additive α → Multiplicative α сохраняет строгий порядок: ofAdd a < ofAdd b ⇔ a < b.

LaTeX

$$$\operatorname{ofAdd} a < \operatorname{ofAdd} b \iff a < b$$$

Lean4

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

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

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

Разделы

Аффилиация

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