∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (x y : M₁),
  (B x) y = ⇑(b.repr x) ⬝ᵥ ((LinearMap.BilinForm.toMatrix b) B).mulVec ⇑(b.repr y)