Commit 2025-08-22 20:24 ecc316fb

View on Github →

refactor: Use StrongDual (#28726) The StrongDual abbrev for M →L[R] R, where the monoid M is a module over the semiring R and R and M are equipped with topologies, was introduced in #27699. This PR replaces existing occurrences of M →L[R] R with StrongDual R M etc. There are some exclusions:

  • Bilinear forms M →L[R] E →L[R] R and where using StrongDual R M would mask the symmetry of the statement;
  • The dual of rings / fields R →L[R] R and similar;
  • WeakDual 𝕜 M in Topology/Algebra/Module/WeakDual, where the focus is on the weak topology on M →L[R] R.

Estimated changes

modified theorem ContDiff.smulRight
modified theorem ContDiffAt.smulRight
modified theorem ContDiffOn.smulRight
modified theorem ContDiffWithinAt.smulRight
modified theorem domain_mvt
modified theorem exists_dual_vector''
modified theorem exists_dual_vector'
modified theorem exists_dual_vector
modified theorem exists_extension_norm_eq
modified theorem RCLike.re_extendTo𝕜'ₗ
modified theorem RCLike.imCLM_apply
modified theorem RCLike.imCLM_coe
modified theorem RCLike.reCLM_apply
modified theorem RCLike.reCLM_coe
modified theorem RCLike.reCLM_norm
modified theorem HasFDerivAt.clog
modified theorem HasFDerivWithinAt.clog
modified theorem HasStrictFDerivAt.clog
modified def TrivSqZeroExt.fstCLM