Structures · Algebra

DivInvMonoid

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

Shape

One type argument · adds div_eq_mul_inv, zpow_zero', zpow_succ', zpow_neg'