∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₁' : Type u_8} {M₂' : Type u_9} {n : Type u_11} {m : Type u_12}
  {n' : Type u_13} {m' : Type u_14} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m]
  [inst_8 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : AddCommMonoid M₁']
  [inst_10 : Module R M₁'] [inst_11 : AddCommMonoid M₂'] [inst_12 : Module R M₂'] (b₁' : Module.Basis n' R M₁')
  (b₂' : Module.Basis m' R M₂') [inst_13 : Fintype n'] [inst_14 : Fintype m'] [inst_15 : DecidableEq n']
  [inst_16 : DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R),
  M * (LinearMap.toMatrix₂ b₁ b₂) B * N =
    (LinearMap.toMatrix₂ b₁' b₂') (B.compl₁₂ ((Matrix.toLin b₁' b₁) M.transpose) ((Matrix.toLin b₂' b₂) N))