min_div_div_right'

Mathlib.Algebra.Order.Group.MinMax

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive min_sub_sub_right]
theorem min_div_div_right' (a b c : α) : min (a / c) (b / c) = min a b / c := by
  simpa only [div_eq_mul_inv] using min_mul_mul_right a b c⁻¹

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

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

Разделы

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

Аффилиация

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