feat(topology/algebra/module/basic): A continuous linear functional i…

…s open (#13829)

src/topology/algebra/module/basic.lean

@@ -501,6 +501,9 @@ coe_injective.unique
 instance unique_of_right [subsingleton M₂] : unique (M₁ →SL[σ₁₂] M₂) :=
 coe_injective.unique
 
+lemma exists_ne_zero {f : M₁ →SL[σ₁₂] M₂} (hf : f ≠ 0) : ∃ x, f x ≠ 0 :=
+by { by_contra' h, exact hf (continuous_linear_map.ext h) }
+
 section
 
 variables (R₁ M₁)
@@ -1025,6 +1028,19 @@ end
 
 end ring
 
+section division_monoid
+variables {R M : Type*}
+
+/-- A nonzero continuous linear functional is open. -/
+protected lemma is_open_map_of_ne_zero [topological_space R] [division_ring R]
+  [has_continuous_sub R] [add_comm_group M] [topological_space M] [has_continuous_add M]
+  [module R M] [has_continuous_smul R M] (f : M →L[R] R) (hf : f ≠ 0) : is_open_map f :=
+let ⟨x, hx⟩ := exists_ne_zero hf in is_open_map.of_sections $ λ y,
+    ⟨λ a, y + (a - f y) • (f x)⁻¹ • x, continuous.continuous_at $ by continuity,
+      by simp, λ a, by simp [hx]⟩
+
+end division_monoid
+
 section smul_monoid
 
 -- The M's are used for semilinear maps, and the N's for plain linear maps