From 5a4bae1158b5503def0d5b417c82578bc1b7b009 Mon Sep 17 00:00:00 2001 From: Eric Rodriguez Date: Tue, 19 Apr 2022 10:05:03 +0000 Subject: [PATCH] feat(algebra/*/basic): add trivial lemmas (#13416) These save you from having to fiddle with `mul_one` when you want to rewrite them the other way, or allow easier commutativity rewrites. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> --- src/algebra/group/basic.lean | 8 ++++++++ src/algebra/ring/basic.lean | 18 ++++++++++++++++++ 2 files changed, 26 insertions(+) diff --git a/src/algebra/group/basic.lean b/src/algebra/group/basic.lean index f284d8504570b..a204850bec373 100644 --- a/src/algebra/group/basic.lean +++ b/src/algebra/group/basic.lean @@ -104,6 +104,14 @@ right_comm has_mul.mul mul_comm mul_assoc theorem mul_mul_mul_comm (a b c d : G) : (a * b) * (c * d) = (a * c) * (b * d) := by simp only [mul_left_comm, mul_assoc] +@[to_additive] +lemma mul_rotate (a b c : G) : a * b * c = b * c * a := +by simp only [mul_left_comm, mul_comm] + +@[to_additive] +lemma mul_rotate' (a b c : G) : a * (b * c) = b * (c * a) := +by simp only [mul_left_comm, mul_comm] + end comm_semigroup local attribute [simp] mul_assoc sub_eq_add_neg diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean index c6dd76f349319..57bcef0fa13e1 100644 --- a/src/algebra/ring/basic.lean +++ b/src/algebra/ring/basic.lean @@ -231,6 +231,15 @@ end non_unital_semiring section non_assoc_semiring variables [non_assoc_semiring α] +lemma add_one_mul (a b : α) : (a + 1) * b = a * b + b := +by rw [add_mul, one_mul] +lemma mul_add_one (a b : α) : a * (b + 1) = a * b + a := +by rw [mul_add, mul_one] +lemma one_add_mul (a b : α) : (1 + a) * b = b + a * b := +by rw [add_mul, one_mul] +lemma mul_one_add (a b : α) : a * (1 + b) = a + a * b := +by rw [mul_add, mul_one] + theorem two_mul (n : α) : 2 * n = n + n := eq.trans (right_distrib 1 1 n) (by simp) @@ -855,6 +864,15 @@ protected def function.surjective.non_assoc_ring { .. hf.add_comm_group f zero add neg sub nsmul gsmul, .. hf.mul_zero_class f zero mul, .. hf.distrib f add mul, .. hf.mul_one_class f one mul } +lemma sub_one_mul (a b : α) : (a - 1) * b = a * b - b := +by rw [sub_mul, one_mul] +lemma mul_sub_one (a b : α) : a * (b - 1) = a * b - a := +by rw [mul_sub, mul_one] +lemma one_sub_mul (a b : α) : (1 - a) * b = b - a * b := +by rw [sub_mul, one_mul] +lemma mul_one_sub (a b : α) : a * (1 - b) = a - a * b := +by rw [mul_sub, mul_one] + end non_assoc_ring /-- A ring is a type with the following structures: additive commutative group (`add_comm_group`),