instCommGroup — Mathlib

English

The Grothendieck group GrothendieckGroup M is a commutative group; the group operations are inherited from the localization construction.

Русский

Группа Гротендик GrothendieckGroup M образует коммутативную группу; операции группы определены через локализацию.

LaTeX

$$$\\mathrm{GrothendieckGroup}(M) \\text{ is a }\\text{Abelian group}$$$

Lean4

/-- The Grothendieck group is a group. -/
@[to_additive /-- The Grothendieck group is a group. -/
    ]
instance instCommGroup : CommGroup (GrothendieckGroup M)
    where
  __ : CommMonoid (GrothendieckGroup M) := inferInstance
  inv_mul_cancel
    a := by
    cases a using ind
    rw [inv_mk, mk_eq_monoidOf_mk', ← Submonoid.LocalizationMap.mk'_mul]
    convert Submonoid.LocalizationMap.mk'_self' _ _
    rw [mul_comm, Submonoid.coe_mul]

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