divp_divp_eq_divp_mul — Mathlib

English

Dividing by u1 and then by u2 equals dividing by u2 · u1: x /ₚ u1 /ₚ u2 = x /ₚ (u2 · u1).

Русский

Последовательное деление на u1 затем на u2 эквивалентно делению на u2 · u1: x /ₚ u1 /ₚ u2 = x /ₚ (u2 · u1).

LaTeX

$$$x /ₚ u_1 /ₚ u_2 = x /ₚ (u_2 \cdot u_1)$$$

Lean4

theorem divp_divp_eq_divp_mul (x : α) (u₁ u₂ : αˣ) : x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁) := by
  simp only [divp, mul_inv_rev, Units.val_mul, mul_assoc]

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