chore(algebra/star/basic): split out big_operators import (#17792)

cf #17772 (comment), cc @eric-wieser
leanprover-community · Dec 3, 2022 · 6f6739f · 6f6739f
1 parent 9114ddf
commit 6f6739f
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 21 deletions.
diff --git a/archive/100-theorems-list/42_inverse_triangle_sum.lean b/archive/100-theorems-list/42_inverse_triangle_sum.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jalex Stark, Yury Kudryashov
 -/
+import algebra.big_operators.basic
 import data.real.basic
 
 /-!

diff --git a/src/algebra/star/basic.lean b/src/algebra/star/basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import algebra.big_operators.basic
 import algebra.ring.aut
 import algebra.ring.comp_typeclasses
 import data.rat.cast
@@ -39,6 +38,8 @@ positive cone which is the closure of the sums of elements `star r * r`. A weake
 advantage of not requiring a topology.
 -/
 
+assert_not_exists finset
+assert_not_exists subgroup
 
 universes u v
 
@@ -165,16 +166,6 @@ op_injective $
   star (x / y) = star x / star y :=
 map_div (star_mul_aut : R ≃* R) _ _
 
-section
-open_locale big_operators
-
-@[simp] lemma star_prod [comm_monoid R] [star_semigroup R] {α : Type*}
-  (s : finset α) (f : α → R):
-  star (∏ x in s, f x) = ∏ x in s, star (f x) :=
-map_prod (star_mul_aut : R ≃* R) _ _
-
-end
-
 /--
 Any commutative monoid admits the trivial `*`-structure.
 
@@ -240,16 +231,6 @@ star_eq_zero.not
   star (n • x) = n • star x :=
 (star_add_equiv : R ≃+ R).to_add_monoid_hom.map_zsmul _ _
 
-section
-open_locale big_operators
-
-@[simp] lemma star_sum [add_comm_monoid R] [star_add_monoid R] {α : Type*}
-  (s : finset α) (f : α → R):
-  star (∑ x in s, f x) = ∑ x in s, star (f x) :=
-(star_add_equiv : R ≃+ R).map_sum _ _
-
-end
-
 /--
 A `*`-ring `R` is a (semi)ring with an involutive `star` operation which is additive
 which makes `R` with its multiplicative structure into a `*`-semigroup

diff --git a/src/algebra/star/big_operators.lean b/src/algebra/star/big_operators.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.big_operators.basic
+import algebra.star.basic
+
+/-! # Big-operators lemmas about `star` algebraic operations
+
+These results are kept separate from `algebra.star.basic` to avoid it needing to import `finset`.
+-/
+
+variables {R : Type*}
+
+open_locale big_operators
+
+@[simp] lemma star_prod [comm_monoid R] [star_semigroup R] {α : Type*}
+  (s : finset α) (f : α → R):
+  star (∏ x in s, f x) = ∏ x in s, star (f x) :=
+map_prod (star_mul_aut : R ≃* R) _ _
+
+@[simp] lemma star_sum [add_comm_monoid R] [star_add_monoid R] {α : Type*}
+  (s : finset α) (f : α → R):
+  star (∑ x in s, f x) = ∑ x in s, star (f x) :=
+(star_add_equiv : R ≃+ R).map_sum _ _
diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean
@@ -10,6 +10,7 @@ import algebra.big_operators.ring
 import algebra.big_operators.ring_equiv
 import algebra.module.linear_map
 import algebra.module.pi
+import algebra.star.big_operators
 import algebra.star.module
 import algebra.star.pi
 import data.fintype.big_operators