Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-08 18:01 dd16a836

View on Github →

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.

Estimated changes