div_mul_cancel_right — Mathlib

English

In a DivisionMonoid, for any a and unit c, a·c / (a·c) = 1; equivalently, (a·c) cancels to 1.

Русский

В делимом моноиде, для любого a и единицы c, a·c / (a·c) = 1; тождество единице.

LaTeX

$$$\forall {\alpha} [DivisionMonoid\ \alpha] {a} {c} (hc : IsUnit c), (a\cdot c) / (a\cdot c) = 1$$$

Lean4

@[to_additive]
protected theorem div_mul_cancel_right (h : IsUnit b) (a : α) : b / (a * b) = a⁻¹ := by
  rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]

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