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.
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.