Theorems · Inductive type · group theory

SubNegMonoid

Type u → Type u

A SubNegMonoid is an AddMonoid with unary - and binary - operations satisfying sub_eq_add_neg : ∀ a b, a - b = a + -b. The default for sub is such that a - b = a + -b holds by definition. Adding sub as a field rather than defining a - b := a + -b allows us to avoid certain classes of unification failures, for example: Let foo X be a type with a ∀ X, Sub (Foo X) instance but no ∀ X, Neg (Foo X). Suppose we also have an instance ∀ X [Cromulent X], AddGroup (Foo X). Then the (-) coming from AddGroup.sub cannot be definitionally equal to the (-) coming from Foo.Sub. In the same way, adding a zsmul field makes it possible to avoid definitional failures in diamonds. See the definition of AddMonoid and Note [forgetful inheritance] for more explanations on this.

Defined in

Mathlib.Algebra.Group.Defs

Cited by

79 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms