Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-10-07 19:06
57004e72
View on Github →
chore(Analysis/LocallyConvex): deprecate
polar_weak_closed
(
#28390
)
Estimated changes
Modified
Mathlib/Analysis/LocallyConvex/Polar.lean
deleted
theorem
LinearMap.polar_weak_closed