Commit 2026-04-03 20:10 7d2c1deb

View on Github →

chore(Analysis/Normed/Module/WeakDual): revert polar, polar_def and isClosed_polar to weaker hypotheses (#37314) The three results mentioned inadvertently had their hypotheses strengthened in [#36332](https://github.com/leanprover-community/mathlib4/pull/36332). This PR recovers generality. In addition, I have globalized variables to guard against this issue happening again and have moved part of a file that does not require NontriviallyNormedField k to Topology/Algebra/Module/WeakDual.

Estimated changes

Modified Mathlib/Analysis/Normed/Module/WeakDual.lean

deleted theorem StrongDual.coe_toWeakDual

deleted def StrongDual.toWeakDual

deleted theorem StrongDual.toWeakDual_apply

deleted theorem StrongDual.toWeakDual_inj

deleted theorem WeakDual.coe_toStrongDual

modified theorem WeakDual.exists_countable_separating

modified theorem WeakDual.isClosed_polar

modified theorem WeakDual.isSeqCompact_closedBall

modified theorem WeakDual.isSeqCompact_of_isBounded_of_isClosed

modified theorem WeakDual.isSeqCompact_polar

modified def WeakDual.polar

modified theorem WeakDual.polar_def

deleted def WeakDual.toStrongDual

deleted theorem WeakDual.toStrongDual_apply

deleted theorem WeakDual.toStrongDual_inj

Modified Mathlib/Topology/Algebra/Module/WeakDual.lean

added theorem StrongDual.coe_toWeakDual

added def StrongDual.toWeakDual

added theorem StrongDual.toWeakDual_apply

added theorem StrongDual.toWeakDual_inj

added theorem WeakDual.coe_toStrongDual

added def WeakDual.toStrongDual

added theorem WeakDual.toStrongDual_apply

added theorem WeakDual.toStrongDual_inj