mathlib

a4dddb59 - chore(topology/algebra/module/weak_dual): golf `weak_dual.t2_space` (#16816)