refactor(algebra/star/*): Allow for star operation on non-associative algebras

src/algebra/algebra/unitization.lean

@@ -408,8 +408,7 @@ instance [comm_semiring R] [star_ring R] [add_comm_monoid A] [star_add_monoid A]
 { star_smul := λ r x, ext (by simp) (by simp) }
 
 instance [comm_semiring R] [star_ring R] [non_unital_semiring A] [star_ring A]
-  [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] [star_module R A] :
-  star_ring (unitization R A) :=
+  [module R A] [star_module R A] : star_ring (unitization R A) :=
 { star_mul := λ x y, ext (by simp [star_mul])
     (by simp [star_mul, add_comm (star x.fst • star y.snd)]),
   ..unitization.star_add_monoid }

src/algebra/star/basic.lean

@@ -117,7 +117,7 @@ attribute [simp] star_trivial
 A `*`-semigroup is a semigroup `R` with an involutive operations `star`
 so `star (r * s) = star s * star r`.
 -/
-class star_semigroup (R : Type u) [semigroup R] extends has_involutive_star R :=
+class star_semigroup (R : Type u) [has_mul R] extends has_involutive_star R :=
 (star_mul : ∀ r s : R, star (r * s) = star s * star r)
 
 export star_semigroup (star_mul)
@@ -236,12 +236,12 @@ A `*`-ring `R` is a (semi)ring with an involutive `star` operation which is addi
 which makes `R` with its multiplicative structure into a `*`-semigroup
 (i.e. `star (r * s) = star s * star r`).
 -/
-class star_ring (R : Type u) [non_unital_semiring R] extends star_semigroup R :=
+class star_ring (R : Type u) [non_unital_non_assoc_semiring R] extends star_semigroup R :=
 (star_add : ∀ r s : R, star (r + s) = star r + star s)
 
 @[priority 100]
-instance star_ring.to_star_add_monoid [non_unital_semiring R] [star_ring R] : star_add_monoid R :=
-{ star_add := star_ring.star_add }
+instance star_ring.to_star_add_monoid [non_unital_non_assoc_semiring R] [star_ring R] :
+star_add_monoid R := { star_add := star_ring.star_add }
 
 /-- `star` as an `ring_equiv` from `R` to `Rᵐᵒᵖ` -/
 @[simps apply]

src/algebra/star/pi.lean

@@ -29,13 +29,13 @@ lemma star_def [Π i, has_star (f i)] (x : Π i, f i) : star x = λ i, star (x i
 instance [Π i, has_involutive_star (f i)] : has_involutive_star (Π i, f i) :=
 { star_involutive := λ _, funext $ λ _, star_star _ }
 
-instance [Π i, semigroup (f i)] [Π i, star_semigroup (f i)] : star_semigroup (Π i, f i) :=
+instance [Π i, has_mul (f i)] [Π i, star_semigroup (f i)] : star_semigroup (Π i, f i) :=
 { star_mul := λ _ _, funext $ λ _, star_mul _ _ }
 
 instance [Π i, add_monoid (f i)] [Π i, star_add_monoid (f i)] : star_add_monoid (Π i, f i) :=
 { star_add := λ _ _, funext $ λ _, star_add _ _ }
 
-instance [Π i, non_unital_semiring (f i)] [Π i, star_ring (f i)] : star_ring (Π i, f i) :=
+instance [Π i, non_unital_non_assoc_semiring (f i)] [Π i, star_ring (f i)] : star_ring (Π i, f i) :=
 { ..pi.star_add_monoid, ..(pi.star_semigroup : star_semigroup (Π i, f i)) }
 
 instance {R : Type w}
@@ -62,3 +62,7 @@ lemma star_sum_elim {I J α : Type*} (x : I → α) (y : J → α) [has_star α]
 by { ext x, cases x; simp }
 
 end function
+
+instance _root_.function.star_module (α β : Type*) [has_star α] [has_star β] [has_smul α β]
+[star_module α β] : star_module α (I → β) :=
+pi.star_module

src/algebra/star/self_adjoint.lean

@@ -6,6 +6,7 @@ Authors: Frédéric Dupuis
 
 import algebra.star.basic
 import group_theory.subgroup.basic
+import algebra.star.pi
 
 /-!
 # Self-adjoint, skew-adjoint and normal elements of a star additive group
@@ -63,11 +64,11 @@ lemma star_iff [has_involutive_star R] {x : R} : is_self_adjoint (star x) ↔ is
 by simpa only [is_self_adjoint, star_star] using eq_comm
 
 @[simp]
-lemma star_mul_self [semigroup R] [star_semigroup R] (x : R) : is_self_adjoint (star x * x) :=
+lemma star_mul_self [has_mul R] [star_semigroup R] (x : R) : is_self_adjoint (star x * x) :=
 by simp only [is_self_adjoint, star_mul, star_star]
 
 @[simp]
-lemma mul_star_self [semigroup R] [star_semigroup R] (x : R) : is_self_adjoint (x * star x) :=
+lemma mul_star_self [has_mul R] [star_semigroup R] (x : R) : is_self_adjoint (x * star x) :=
 by simpa only [star_star] using star_mul_self (star x)
 
 /-- Functions in a `star_hom_class` preserve self-adjoint elements. -/
@@ -274,7 +275,12 @@ instance : has_rat_cast (self_adjoint R) :=
 rfl
 
 instance has_qsmul : has_smul ℚ (self_adjoint R) :=
-⟨λ a x, ⟨a • x, by rw rat.smul_def; exact (rat_cast_mem a).mul x.prop⟩⟩
+⟨λ a x, ⟨a • x, by rw rat.smul_def;
+  begin
+    apply is_self_adjoint.mul,
+    exact rat_cast_mem a,
+    exact x.prop,
+  end ⟩ ⟩
 
 @[simp, norm_cast] lemma coe_rat_smul (x : self_adjoint R) (a : ℚ) : ↑(a • x) = a • (x : R) :=
 rfl