Theorems · Inductive type · nonassociative algebras

Bracket

Type u_1 → Type u_2 → Type (max u_1 u_2)

The Bracket class has three intended uses: 1. for certain binary operations on structures, like the product ⁅x, y⁆ of two elements x, y in a Lie algebra or the commutator of two elements x and y in a group. 2. for certain actions of one structure on another, like the action ⁅x, m⁆ of an element x of a Lie algebra on an element m in one of its modules (analogous to SMul in the associative setting). 3. for binary operations on substructures, like the commutator ⁅H, K⁆ of two subgroups H and K of a group.

Defined in

Mathlib.Data.Bracket

Cited by

8 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms