mathlib

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