toDivisionMonoid — Mathlib

English

A group G can be endowed with a CancelMonoid structure.

Русский

Группа G может быть наделена структурой CancelMonoid.

LaTeX

$$$G \\text{ is CancelMonoid}$$$

Lean4

@[to_additive]
instance (priority := 100) toDivisionMonoid : DivisionMonoid G :=
  { inv_inv := fun a ↦ inv_eq_of_mul (inv_mul_cancel a)
    mul_inv_rev := fun a b ↦ inv_eq_of_mul <| by rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]
    inv_eq_of_mul := fun _ _ ↦ inv_eq_of_mul }
    -- see Note [lower instance priority]

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