Theorems · Inductive type · group theory

Group

Type u → Type u

A Group is a Monoid with an operation ⁻¹ satisfying a⁻¹ * a = 1. There is also a division operation / such that a / b = a * b⁻¹, with a default so that a / b = a * b⁻¹ holds by definition. Use Group.ofLeftAxioms or Group.ofRightAxioms to define a group structure on a type with the minimum proof obligations. [Wikidata Q83478](https://www.wikidata.org/wiki/Q83478)

Defined in

Mathlib.Algebra.Group.Defs

Cited by

6,238 results in Mathlib

Foundations

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