Zulip Chat Archive

Stream: general

Topic: algebra classes


view this post on Zulip Kenny Lau (May 10 2020 at 05:41):

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))

Last updated: May 15 2021 at 00:39 UTC