div_eq_div_iff_comm

Mathlib.Algebra.Group.Basic

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

English

For all a,b,c,d ∈ α, a / b = c / d if and only if b / a = d / c.

Русский

Для всех a,b,c,d ∈ α верно: a / b = c / d тогда и только тогда, когда b / a = d / c.

LaTeX

$$$a / b = c / d \\iff b / a = d / c$$$

Lean4

@[to_additive]
theorem div_eq_div_iff_comm : a / b = c / d ↔ b / a = d / c :=
  inv_inj.symm.trans <| by simp only [inv_div]

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

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

Разделы

Аффилиация

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