feat(topology/algebra/module/basic): A continuous linear functional is open (#13829)
feat(topology/algebra/module/basic): A continuous linear functional is open (#13829)






leanprover-community/mathlib,leanprover-community/mathlib