mathlib3

dd16a836 - fix(topology/algebra/module/weak_dual): fix namespace issue, add a few extra lemmas (#13407)

fix(topology/algebra/module/weak_dual): fix namespace issue, add a few extra lemmas (#13407) This PR fixes a namespace issue in `weak_dual`, to ensure lemmas with names like `eval_continuous` are appropriately namespaced. Also, lemmas about continuity of the evaluation map have been copied from `weak_bilin` to `weak_dual`. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>