feat port Algebra.GroupPower.Lemmas (#1055)

aba57d4d3dae35460225919dcd82fe91355162f9 - [x] depends on #1043 - [x] depends on #1050 Co-authored-by: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
leanprover-community · Dec 19, 2022 · 1bec125 · 1bec125
1 parent 94dfa4b
commit 1bec125
Show file tree

Hide file tree

Showing 4 changed files with 1,303 additions and 18 deletions.
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
@@ -361,6 +361,14 @@ theorem div_mul_eq_div_div_swap : a / (b * c) = a / c / b :=
 
 end DivisionMonoid
 
+section SubtractionMonoid
+
+set_option linter.deprecated false
+
+lemma bit0_neg [SubtractionMonoid α] (a : α) : bit0 (-a) = -bit0 a := (neg_add_rev _ _).symm
+
+end SubtractionMonoid
+
 section DivisionCommMonoid
 
 variable [DivisionCommMonoid α] (a b c d : α)