feat: add scalar tower instances for RingQuot and BilinForm

Mathlib/Algebra/RingQuot.lean

@@ -269,6 +269,14 @@ theorem smul_quot [Algebra S R] {n : S} {a : R} :
   rfl
 #align ring_quot.smul_quot RingQuot.smul_quot
 
+instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [IsScalarTower S T R] :
+    IsScalarTower S T (RingQuot r) :=
+  ⟨fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_assoc]⟩
+
+instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] :
+    SMulCommClass S T (RingQuot r) :=
+  ⟨fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_comm]⟩
+
 instance instAddCommMonoid (r : R → R → Prop) : AddCommMonoid (RingQuot r) where
   add := (· + ·)
   zero := 0

Mathlib/LinearAlgebra/BilinearForm.lean

@@ -223,6 +223,21 @@ theorem smul_apply {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R
   rfl
 #align bilin_form.smul_apply BilinForm.smul_apply
 
+instance {α β} [Monoid α] [Monoid β] [DistribMulAction α R] [DistribMulAction β R]
+    [SMulCommClass α R R] [SMulCommClass β R R] [SMulCommClass α β R] :
+    SMulCommClass α β (BilinForm R M) :=
+  ⟨fun a b B => ext $ fun x y => smul_comm a b (B x y)⟩
+
+instance {α β} [Monoid α] [Monoid β] [SMul α β] [DistribMulAction α R] [DistribMulAction β R]
+    [SMulCommClass α R R] [SMulCommClass β R R] [IsScalarTower α β R] :
+    IsScalarTower α β (BilinForm R M) :=
+  ⟨fun a b B => ext $ fun x y => smul_assoc a b (B x y)⟩
+
+instance {α} [Monoid α] [DistribMulAction α R] [DistribMulAction αᵐᵒᵖ R]
+    [SMulCommClass α R R] [IsCentralScalar α R] :
+    IsCentralScalar α (BilinForm R M) :=
+  ⟨fun a B => ext $ fun x y => op_smul_eq_smul a (B x y)⟩
+
 instance : AddCommMonoid (BilinForm R M) :=
   Function.Injective.addCommMonoid _ coe_injective coe_zero coe_add fun _ _ => coe_smul _ _