mul_div_mul_right — Mathlib

English

For any α with DivisionMonoid and any unit c, a·c / (b·c) = a / b for all a,b.

Русский

Для α с DivisionMonoid и любой единицы c, a·c / (b·c) = a / b для любых a,b.

LaTeX

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

Lean4

@[to_additive]
protected theorem mul_div_mul_right (h : IsUnit c) (a b : α) : a * c / (b * c) = a / b := by
  simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]

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