eq_iff_eq_of_div_eq_div

Mathlib.Algebra.Group.Basic

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

English

If a / b = c / d, then a = b ⇔ c = d.

Русский

Если a / b = c / d, то a = b ⇔ c = d.

LaTeX

$$$\forall a,b,c,d \in G,\ a/b = c/d \Rightarrow (a=b) \Leftrightarrow (c=d).$$

Lean4

@[to_additive]
theorem eq_iff_eq_of_div_eq_div (H : a / b = c / d) : a = b ↔ c = d := by rw [← div_eq_one, H, div_eq_one]

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

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

Разделы

Аффилиация

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