Theorem LinearMap.polar_nonempty

Modification history

2024-09-23 18:06
Mathlib/Analysis/LocallyConvex/Polar.lean
feature(Analysis/Normed/Module/Dual): Add a few polar lemmas (#16426) …
Added LinearMap.polar_nonemptyView on Github →