∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (h : PowerBasis R S),
  (LinearMap.BilinForm.toMatrix h.basis) (Algebra.traceForm R S) =
    Matrix.of fun i j => (Algebra.trace R S) (h.gen ^ (↑i + ↑j))