Commit 2025-09-11 04:25 3761bc35

View on Github →

chore(Topology/Algebra/Module/StrongDual): remove strongDualPairing and move contents (#29320) This PR deletes strongDualPairing, which is a duplicate of topDualPairing. The other contents of the file are moved to Mathlib.Analysis.LocallyConvex.Polar, because they are specializations of the general theory of polars, and they do not actually use the strong topology on the dual.

Estimated changes

added def StrongDual.polar
added theorem StrongDual.polar_empty
added theorem StrongDual.polar_univ
added theorem StrongDual.polar_zero
added def topDualPairing
added theorem topDualPairing_apply
deleted theorem StrongDual.mem_polar_iff
deleted def StrongDual.polar
deleted theorem StrongDual.polar_empty
deleted theorem StrongDual.polar_nonempty
deleted theorem StrongDual.polar_univ
deleted theorem StrongDual.polar_zero
deleted theorem StrongDual.zero_mem_polar
deleted def strongDualPairing
deleted def topDualPairing
deleted theorem topDualPairing_apply