𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type ?u.39284
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ Function.Injective ↑(dualPairing 𝕜 E)
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type ?u.39284
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ LinearMap.SeparatingLeft (dualPairing 𝕜 E)
rw [LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.ker_eq_bot]
no goals
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type ?u.39284
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ Function.Injective ↑(dualPairing 𝕜 E)
exact ContinuousLinearMap.coe_injective