mul_divp_cancel — Mathlib

English

Multiplying by a unit on the left and then dividing by that unit returns the original element: a · u /ₚ u = a.

Русский

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

LaTeX

$$$a \cdot u /ₚ u = a$$$

Lean4

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

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