mk_div_eq_mk_left

Mathlib.Algebra.Order.Archimedean.Class

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mk_div_eq_mk_left (h : mk a < mk b) : mk (a / b) = mk a := by
  simpa [h, div_eq_mul_inv] using mk_mul_eq_mk_left (a := a) (b := b⁻¹)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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