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 #
has_bracket L M for a binary operation that takes something in
L and something in
produces something in
M. Defining an instance of this structure gives access to the 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.
The has_bracket class has three intended uses:
for certain binary operations on structures, like the product
⁅x, y⁆ of two elements
y in a Lie algebra or the commutator of two elements
y in a group.
for certain actions of one structure on another, like the action
⁅x, m⁆ of an element
of a Lie algebra on an element
m in one of its modules (analogous to
has_smul in the
for binary operations on substructures, like the commutator
⁅H, K⁆ of two subgroups
K of a group.
Instances of this typeclass
Instances of other typeclasses for