∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} {o : Type u_6} [inst_3 : Fintype n] [inst_4 : Fintype o] [inst_5 : DecidableEq n]
  (b : Module.Basis n R₁ M₁) {M₂' : Type u_7} [inst_6 : AddCommMonoid M₂'] [inst_7 : Module R₁ M₂']
  (c : Module.Basis o R₁ M₂') [inst_8 : DecidableEq o] (B : LinearMap.BilinForm R₁ M₁) (l r : M₂' →ₗ[R₁] M₁),
  (LinearMap.BilinForm.toMatrix c) (B.comp l r) =
    ((LinearMap.toMatrix c b) l).transpose * (LinearMap.BilinForm.toMatrix b) B * (LinearMap.toMatrix c b) r