divp_mul_divp — Mathlib

English

For α a commutative monoid and ux, uy units, x /ₚ ux · (y /ₚ uy) = x · y /ₚ (ux · uy).

Русский

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

LaTeX

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

Lean4

theorem divp_mul_divp (x y : α) (ux uy : αˣ) : x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy) := by
  rw [divp_mul_eq_mul_divp, ← divp_assoc, divp_divp_eq_divp_mul]

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