mathlib3 documentation

data.bracket

Bracket Notation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides notation which can be used for the Lie bracket, for the commutator of two subgroups, and for other similar operations.

Main Definitions #

Notation #

We introduce the notation ⁅x, y⁆ for the bracket of any has_bracket structure. Note that these are the Unicode "square with quill" brackets rather than the usual square brackets.

@[class]
structure has_bracket (L : Type u_1) (M : Type u_2) :
Type (max u_1 u_2)

The has_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 has_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.

Instances of this typeclass
Instances of other typeclasses for has_bracket
  • has_bracket.has_sizeof_inst