max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/algebra/classes): typos

Browse source
This commit is contained in:
Leonardo de Moura 2018-01-10 15:17:02 -08:00
parent 26da50ab0e
commit fc760f57d2
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/algebra/classes.lean
View file

@ -40,16 +40,16 @@ universes u
@[algebra] class is_right_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param $ α → α → α) : Prop :=
(right_distrib : ∀ a b c, op₁ (op₂ a b) c = op₂ (op₁ a c) (op₁ b c))
@[algebra] class is_left_inv (α : Type u) (op : α → α → α) (inv : out_param α → α) (o : out_param $ α) : Prop :=
@[algebra] class is_left_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param α) : Prop :=
(left_inv : ∀ a, op (inv a) a = o)
@[algebra] class is_right_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param $ α) : Prop :=
@[algebra] class is_right_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param α) : Prop :=
(right_inv : ∀ a, op a (inv a) = o)
@[algebra] class is_cond_left_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param $ α) (p : out_param $ α → Prop) : Prop :=
@[algebra] class is_cond_left_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param α) (p : out_param $ α → Prop) : Prop :=
(left_inv : ∀ a, p a → op (inv a) a = o)
@[algebra] class is_cond_right_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param $ α) (p : out_param $ α → Prop) : Prop :=
@[algebra] class is_cond_right_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param α) (p : out_param $ α → Prop) : Prop :=
(right_inv : ∀ a, p a → op a (inv a) = o)
@[algebra] class is_distinct (α : Type u) (a : α) (b : α) : Prop :=