Documentation

Mathlib.Algebra.FreeAbelianGroup.UniqueSums

Free abelian groups have unique sums #

source
instance instTwoUniqueSumsFreeAbelianGroup {σ : Type u_1} :
TwoUniqueSums (FreeAbelianGroup σ)