div_eq_div_of_div_eq_div

Mathlib.Algebra.GroupWithZero.Units.Basic

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

← MathLib Explorer

English

If c,d ≠ 0 and a/b = c/d, then a/c = b/d.

Русский

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

LaTeX

$$$\forall c,d\neq 0:\; a/b=c/d \Rightarrow a/c=b/d$$$

Lean4

theorem div_eq_div_of_div_eq_div (hc : c ≠ 0) (hd : d ≠ 0) (h : a / b = c / d) : a / c = b / d :=
  have hb : b ≠ 0 := by
    intro hb
    rw [hb, div_zero] at h
    exact div_ne_zero hc hd h.symm
  (div_eq_div_iff_div_eq_div' hb hc).mp h

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

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

Разделы

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

Аффилиация

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