div_eq_mul_inv — Mathlib

English

For all a,b in G, the division a / b is equal to a multiplied by b⁻¹: a / b = a · b⁻¹.

Русский

Для всех a, b в G выполняется a / b = a · b⁻¹.

LaTeX

$$$a / b = a b^{-1}$$$

Lean4

/-- Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of `DivInvMonoid.div_eq_mul_inv` ensuring that the types unfold better.
-/
@[to_additive /-- Subtracting an element is the same as adding by its negative.
    This is a duplicate of `SubNegMonoid.sub_eq_add_neg` ensuring that the types unfold better. -/
    ]
theorem div_eq_mul_inv (a b : G) : a / b = a * b⁻¹ :=
  DivInvMonoid.div_eq_mul_inv _ _

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