mk_mul_eq_mk_right

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanClass.mk_mul_eq_mk_right

English

If mk b < mk a, then mk(a b) = mk b.

Русский

Если mk b < mk a, то mk(a b) = mk b.

LaTeX

$$mk b < mk a \Rightarrow mk(a b) = mk b$$

Lean4

@[to_additive]
theorem mk_mul_eq_mk_right (h : mk b < mk a) : mk (a * b) = mk b :=
  mul_comm a b ▸ mk_mul_eq_mk_left h

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

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

Разделы

Аффилиация

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