feat: lift star-preserving actions to actions between unitary groups

Author: j-loreaux

Mathlib/Algebra/Star/Unitary.lean

@@ -172,6 +172,27 @@ lemma _root_.isStarNormal_of_mem_unitary {u : R} (hu : u ∈ unitary R) : IsStar
 
 end Monoid
 
+section SMul
+
+variable {A : Type*} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A]
+    [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A]
+
+instance : SMul (unitary R) (unitary A) where
+  smul r a := ⟨r • a, by
+    simp [Submonoid.smul_def, mem_iff, smul_smul, mul_smul_comm, smul_mul_assoc]⟩
+
+@[simp]
+lemma coe_smul (r : unitary R) (a : unitary A) : ↑(r • a) = r • (a : A) := rfl
+
+instance : MulAction (unitary R) (unitary A) where
+  one_smul _ := Subtype.ext <| one_smul ..
+  mul_smul _ _ _ := Subtype.ext <| mul_smul ..
+
+instance : StarModule (unitary R) (unitary A) where
+  star_smul _ _ := Subtype.ext <| star_smul (_ : R) _
+
+end SMul
+
 section Map
 
 variable {F R S : Type*} [Monoid R] [StarMul R] [Monoid S] [StarMul S]