mul_div_mul_comm — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
protected theorem mul_div_mul_comm (hcd : Commute c d) (hbc : Commute b c⁻¹) : a * b / (c * d) = a / c * (b / d) :=
  (hcd.div_mul_div_comm hbc.symm).symm

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