chore(algebra): move star_ring structure on free_algebra (#12297)

There's no need to have `algebra.star.basic` imported transitively into pretty much everything, just to put the `star_ring` structure on `free_algebra`, so I've moved this construction to its own file.

(I was changing definitions in `algebra.star.basic` to allow for more non-unital structures, it recompiling was very painful because of this transitive dependence.)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/free_algebra.lean

@@ -411,27 +411,5 @@ begin
   exact of_id a,
 end
 
-/-- The star ring formed by reversing the elements of products -/
-instance : star_ring (free_algebra R X) :=
-{ star := mul_opposite.unop ∘ lift R (mul_opposite.op ∘ ι R),
-  star_involutive := λ x, by
-  { unfold has_star.star,
-    simp only [function.comp_apply],
-    refine free_algebra.induction R X _ _ _ _ x; intros; simp [*] },
-  star_mul := λ a b, by simp,
-  star_add := λ a b, by simp }
-
-@[simp]
-lemma star_ι (x : X) : star (ι R x) = (ι R x) :=
-by simp [star, has_star.star]
-
-@[simp]
-lemma star_algebra_map (r : R) : star (algebra_map R (free_algebra R X) r) = (algebra_map R _ r) :=
-by simp [star, has_star.star]
-
-/-- `star` as an `alg_equiv` -/
-def star_hom : free_algebra R X ≃ₐ[R] (free_algebra R X)ᵐᵒᵖ :=
-{ commutes' := λ r, by simp [star_algebra_map],
-  ..star_ring_equiv }
 
 end free_algebra

src/algebra/free_monoid.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yury Kudryashov
 -/
-import algebra.star.basic
+import data.list.big_operators
 
 /-!
 # Free monoid over a given alphabet
@@ -121,16 +121,4 @@ hom_eq $ λ x, rfl
 lemma map_comp (g : β → γ) (f : α → β) : map (g ∘ f) = (map g).comp (map f) :=
 hom_eq $ λ x, rfl
 
-instance : star_monoid (free_monoid α) :=
-{ star := list.reverse,
-  star_involutive := list.reverse_reverse,
-  star_mul := list.reverse_append, }
-
-@[simp]
-lemma star_of (x : α) : star (of x) = of x := rfl
-
-/-- Note that `star_one` is already a global simp lemma, but this one works with dsimp too -/
-@[simp]
-lemma star_one : star (1 : free_monoid α) = 1 := rfl
-
 end free_monoid

src/algebra/module/linear_map.lean

@@ -9,6 +9,7 @@ import algebra.module.basic
 import algebra.module.pi
 import algebra.group_action_hom
 import algebra.ring.comp_typeclasses
+import algebra.star.basic
 
 /-!
 # (Semi)linear maps

src/algebra/star/free.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2020 Eric Weiser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Weiser
+-/
+import algebra.star.basic
+import algebra.free_algebra
+
+/-!
+# A *-algebra structure on the free algebra.
+
+Reversing words gives a *-structure on the free monoid or on the free algebra on a type.
+
+## Implementation note
+We have this in a separate file, rather than in `algebra.free_monoid` and `algebra.free_algebra`,
+to avoid importing `algebra.star.basic` into the entire hierarchy.
+-/
+
+namespace free_monoid
+variables {α : Type*}
+
+instance : star_monoid (free_monoid α) :=
+{ star := list.reverse,
+  star_involutive := list.reverse_reverse,
+  star_mul := list.reverse_append, }
+
+@[simp]
+lemma star_of (x : α) : star (of x) = of x := rfl
+
+/-- Note that `star_one` is already a global simp lemma, but this one works with dsimp too -/
+@[simp]
+lemma star_one : star (1 : free_monoid α) = 1 := rfl
+
+end free_monoid
+
+namespace free_algebra
+variables {R : Type*} [comm_semiring R] {X : Type*}
+
+/-- The star ring formed by reversing the elements of products -/
+instance : star_ring (free_algebra R X) :=
+{ star := mul_opposite.unop ∘ lift R (mul_opposite.op ∘ ι R),
+  star_involutive := λ x, by
+  { unfold has_star.star,
+    simp only [function.comp_apply],
+    refine free_algebra.induction R X _ _ _ _ x; intros; simp [*] },
+  star_mul := λ a b, by simp,
+  star_add := λ a b, by simp }
+
+@[simp]
+lemma star_ι (x : X) : star (ι R x) = (ι R x) :=
+by simp [star, has_star.star]
+
+@[simp]
+lemma star_algebra_map (r : R) : star (algebra_map R (free_algebra R X) r) = (algebra_map R _ r) :=
+by simp [star, has_star.star]
+
+/-- `star` as an `alg_equiv` -/
+def star_hom : free_algebra R X ≃ₐ[R] (free_algebra R X)ᵐᵒᵖ :=
+{ commutes' := λ r, by simp [star_algebra_map],
+  ..star_ring_equiv }
+
+end free_algebra

src/data/nat/factorization.lean

@@ -6,6 +6,7 @@ Authors: Stuart Presnell
 import data.nat.prime
 import data.finsupp.multiset
 import algebra.big_operators.finsupp
+import tactic.linarith
 
 /-!
 # Prime factorizations