{R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : TopologicalSpace R] →
      [inst_2 : ContinuousAdd R] →
        [inst_3 : ContinuousConstSMul R R] →
          {M : Type u_2} →
            [inst_4 : AddCommMonoid M] →
              [inst_5 : TopologicalSpace M] → [inst_6 : Module R M] → StrongDual R M ≃ₗ[R] WeakDual R M