Commit 2025-02-01 08:46 e736b5ac

View on Github →

feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) Definition of the polar of a subspace closed under scalar multiplication as a submodule.

Estimated changes