Theorems · Theorem · group theory

Algebra.GrothendieckGroup.lift_apply

∀ {M : Type u_1} {G : Type u_2} [inst : CommMonoid M] [inst_1 : CommGroup G] (f : M →* G)
  (x : Algebra.GrothendieckGroup M),
  (Algebra.GrothendieckGroup.lift f) x = f ((Localization.monoidOf ⊤).sec x).1 / f ↑((Localization.monoidOf ⊤).sec x).2

Defined in

Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidCommGroup