Structures · Algebra

DivisionMonoid

A DivisionMonoid is a DivInvMonoid with involutive inversion and such that (a * b)⁻¹ = b⁻¹ * a⁻¹ and a * b = 1 → a⁻¹ = b. This is the immediate common ancestor of Group and GroupWithZero.

Defined in

Mathlib.Algebra.Group.Defs

Shape

One type argument · adds inv_inv, mul_inv_rev, inv_eq_of_mul