Commit 2024-09-23 18:06 8192b1ae

View on Github →

feature(Analysis/Normed/Module/Dual): Add a few polar lemmas (#16426) Adds a few trivial polar lemmas. CC: @urkud

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

added theorem LinearMap.polar_nonempty

Modified Mathlib/Analysis/Normed/Module/Dual.lean

added theorem NormedSpace.polar_empty

added theorem NormedSpace.polar_nonempty

added theorem NormedSpace.polar_zero

added theorem NormedSpace.zero_mem_polar