max_div_min_eq_mabs'

Mathlib.Algebra.Order.Group.Unbundled.Abs

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

← MathLib Explorer

English

The ratio max(a,b) / min(a,b) equals |a / b|_m.

Русский

Отношение max(a,b)/min(a,b) равно |a/b|_м.

LaTeX

$$max(a,b) / min(a,b) = |a / b|_m$$

Lean4

@[to_additive]
theorem max_div_min_eq_mabs' (a b : α) : max a b / min a b = |a / b|ₘ :=
  by
  rcases le_total a b with ab | ba
  · rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]
    rwa [div_le_one']
  · rw [max_eq_left ba, min_eq_right ba, mabs_of_one_le]
    rwa [one_le_div']

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

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

Разделы

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

Аффилиация

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