Theorems · Inductive type · group theory

DivInvMonoid

Type u → Type u

A DivInvMonoid is a Monoid with operations / and ⁻¹ satisfying div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹. This deduplicates the name div_eq_mul_inv. The default for div is such that a / b = a * b⁻¹ holds by definition. Adding div 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, Div (Foo X) instance but no ∀ X, Inv (Foo X), e.g. when Foo X is a EuclideanDomain. Suppose we also have an instance ∀ X [Cromulent X], GroupWithZero (Foo X). Then the (/) coming from GroupWithZero.div cannot be definitionally equal to the (/) coming from Foo.Div. In the same way, adding a zpow field makes it possible to avoid definitional failures in diamonds. See the definition of Monoid and Note [forgetful inheritance] for more explanations on this.

Defined in

Mathlib.Algebra.Group.Defs

Cited by

103 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms