div_div_div_cancel_left'

Mathlib.Algebra.GroupWithZero.Units.Basic

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

English

If c ≠ 0, then c / a / (c / b) = b / a for all a,b.

Русский

Если c ≠ 0, то c / a / (c / b) = b / a для любых a,b.

LaTeX

$$$c \\neq 0 \\Rightarrow \\dfrac{c}{a} / \\left( \\dfrac{c}{b} \\right) = \\dfrac{b}{a}$$$

Lean4

theorem div_div_div_cancel_left' (a b : G₀) (hc : c ≠ 0) : c / a / (c / b) = b / a := by
  rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]

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

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

Разделы

Аффилиация

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