Theorem StrongDual.mem_polarSubmodule

Modification history

2025-09-11 04:25

Mathlib/Analysis/LocallyConvex/Polar.lean

chore(Topology/Algebra/Module/StrongDual): remove `strongDualPairing` and move contents (#29320) …

Modified StrongDual.mem_polarSubmodule View on Github →

2025-08-11 22:14

Mathlib/Topology/Algebra/Module/StrongDual.lean

refactor(Analysis/Normed/Module/Dual): Abbrev for strong dual (#27699) …

Added StrongDual.mem_polarSubmodule View on Github →