divp_mul_cancel — Mathlib

English

Canceling by a unit on the right after a divp yields the original element: a /ₚ u · u = a.

Русский

После деления на единицу справа умножение на единицу восстанавливает исходный элемент: a /ₚ u · u = a.

LaTeX

$$$\left(a /ₚ u\right) \cdot u = a$$$

Lean4

@[simp]
theorem divp_mul_cancel (a : α) (u : αˣ) : a /ₚ u * u = a :=
  (mul_assoc _ _ _).trans <| by rw [Units.inv_mul, mul_one]

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