instInv — Mathlib

English

There exists an inverse operation making GrothendieckGroup into a group; i.e., an instance for Inv(GrothendieckGroup M).

Русский

Существование операции обратности, превращающей GrothendieckGroup M в группу; существует инстанс Inv(GrothendieckGroup M).

LaTeX

$$$\\text{Inv}(\\mathrm{GrothendieckGroup}(M))$ exists$$

Lean4

@[to_additive]
instance : Inv (GrothendieckGroup M) where
  inv :=
    rec (fun m s ↦ (.mk s ⟨m, Submonoid.mem_top m⟩ : GrothendieckGroup M)) fun {m₁ m₂ s₁ s₂} h ↦ by
      simpa [r_iff_exists, mk_eq_mk_iff, eq_comm, mul_comm] using h

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