div_div_div_comm — Mathlib

English

If b c and b^{-1} d and c^{-1} d commute appropriately, then a / b / (c / d) = a / c / (b / d).

Русский

Если выполняются необходимые сопряжения между b, c, d и их обратными, то a / b / (c / d) = a / c / (b / d).

LaTeX

$$$ \\text{Commute } b c \\Rightarrow \\text{Commute } b^{-1} d \\Rightarrow \\text{Commute } c^{-1} d \\Rightarrow a / b / (c / d) = a / c / (b / d) $$$

Lean4

@[to_additive]
protected theorem div_div_div_comm (hbc : Commute b c) (hbd : Commute b⁻¹ d) (hcd : Commute c⁻¹ d) :
    a / b / (c / d) = a / c / (b / d) := by
  simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq, hbc.inv_inv.mul_mul_mul_comm]

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