From 5ba5e6666587131d0af57e341da7fbed3331211a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Apr 2015 11:00:59 -0700 Subject: [PATCH] feat(library/algebra/binary): add auxiliary theorems --- library/algebra/binary.lean | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean index 79dd40e1e..5014c4dcd 100644 --- a/library/algebra/binary.lean +++ b/library/algebra/binary.lean @@ -7,9 +7,8 @@ Authors: Leonardo de Moura, Jeremy Avigad General properties of binary operations. -/ - -import logic.eq -open eq.ops +import algebra.function +open eq.ops function namespace binary section @@ -45,7 +44,6 @@ namespace binary definition left_commutative [reducible] {B : Type} (f : A → B → B) := ∀ a₁ a₂ b, f a₁ (f a₂ b) = f a₂ (f a₁ b) end - context variable {A : Type} variable {f : A → A → A} @@ -76,4 +74,11 @@ namespace binary ... = a*((b*c)*d) : H_assoc end + definition right_commutative_compose_right [reducible] + {A B : Type} (f : A → A → A) (g : B → A) (rcomm : right_commutative f) : right_commutative (compose_right f g) := + λ a b₁ b₂, !rcomm + + definition left_commutative_compose_left [reducible] + {A B : Type} (f : A → A → A) (g : B → A) (lcomm : left_commutative f) : left_commutative (compose_left f g) := + λ a b₁ b₂, !lcomm end binary