From fc760f57d20e0a486d14bc8a08d89147b60f530c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Jan 2018 15:17:02 -0800 Subject: [PATCH] chore(library/init/algebra/classes): typos --- library/init/algebra/classes.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/init/algebra/classes.lean b/library/init/algebra/classes.lean index e0276ec4a8..2ae9edfc65 100644 --- a/library/init/algebra/classes.lean +++ b/library/init/algebra/classes.lean @@ -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 :=