max_div_div_right'

Mathlib.Algebra.Order.Group.MinMax

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

← MathLib Explorer

English

In a commutative ordered group, max(a/c, b/c) = max(a,b)/c.

Русский

В коммутативной упорядоченной группе: max(a/c, b/c) = max(a,b)/c.

LaTeX

$$$ \max\left(\frac{a}{c}, \frac{b}{c}\right) = \frac{\max(a,b)}{c} $$$

Lean4

@[to_additive max_sub_sub_right]
theorem max_div_div_right' (a b c : α) : max (a / c) (b / c) = max a b / c := by
  simpa only [div_eq_mul_inv] using max_mul_mul_right a b c⁻¹

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

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

Разделы

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

Аффилиация

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