∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [inst_6 : ContinuousAdd 𝕜] [inst_7 : ContinuousConstSMul 𝕜 𝕜] (x : 𝕜) (x_1 : F),
  { toLinearMap := B.flip (x • x_1), cont := ⋯ } = (RingHom.id 𝕜) x • { toLinearMap := B.flip x_1, cont := ⋯ }