max_div_min_eq_mabs

Mathlib.Algebra.Order.Group.Unbundled.Abs

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

English

The same as above with a swapped, giving max(a,b)/min(a,b) = |b/a|_m.

Русский

То же самое при замене местами: max(a,b)/min(a,b) = |b/a|_м.

LaTeX

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

Lean4

@[to_additive]
theorem max_div_min_eq_mabs (a b : α) : max a b / min a b = |b / a|ₘ := by rw [mabs_div_comm, max_div_min_eq_mabs']

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

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

Разделы

Аффилиация

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