divp_mul_eq_mul_divp — Mathlib

English

For α a commutative monoid and units ux, uy, the division by ux of x times the division by uy of y equals the division by ux*uy of x*y.

Русский

Для коммутативного моноида α и единиц ux, uy имеем: (x /ₚ ux) · (y /ₚ uy) = (x · y) /ₚ (ux · uy).

LaTeX

$$$ x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy) $$$

Lean4

theorem divp_mul_eq_mul_divp (x y : α) (u : αˣ) : x /ₚ u * y = x * y /ₚ u := by rw [divp, divp, mul_right_comm]

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