Theorem LinearMap.polar_weak_closed

Modification history

2025-10-07 19:06

Mathlib/Analysis/LocallyConvex/Polar.lean

chore(Analysis/LocallyConvex): deprecate `polar_weak_closed` (#28390)

Deleted LinearMap.polar_weak_closed View on Github →

2023-04-10 18:08

Mathlib/Analysis/LocallyConvex/Polar.lean

feat: port Analysis.LocallyConvex.Polar (#3367)

Added LinearMap.polar_weak_closed View on Github →