div_mul_div_comm — Mathlib

English

If b and d commute and b^{-1} and c commute in a division monoid, then a/b · (c/d) = a/c · (b/d).

Русский

Если b и d коммутируют и b^{-1} и c коммутируют в делимом моноиде, тогда a/b · (c/d) = a/c · (b/d).

LaTeX

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

Lean4

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

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