algebra classes

Stream: general

[Kenny Lau]

What are the uses of algebra classes such as the following?

@[algebra] class is_symm_op (α : Type u) (β : out_param (Type v)) (op : α → α → β) : Prop :=
(symm_op : ∀ a b, op a b = op b a)

@[algebra] class is_left_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param $ α → α → α) : Prop :=
(left_distrib : ∀ a b c, op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c))