Mathlib.CategoryTheory.Preadditive.Generator._auxLemma.1

theorem Mathlib.CategoryTheory.Preadditive.Generator._auxLemma.1 : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, (a - b = 0) = (a = b)

This theorem states that for any type `G` that forms an additive group, and any two elements `a` and `b` of `G`, the statement "`a` minus `b` equals zero" is equivalent to the statement "`a` equals `b`". In other words, in any additive group, subtracting an element from itself always results in the zero element of that group.

More concisely: In an additive group, for all elements `a` and `b`, `a - b = 0` if and only if `a = b`.