Commit 2026-04-28 19:12 0360dad5

View on Github →

chore(LinearAlgebra/Dual): deprecate Module.dualPairing (#37542)

  • deprecate Module.dualPairing (and associated lemmas) since merely synonym for identity (essentially always easier to just use .id, see next bullet point)
  • remove use of deprecated lemmas
  • remove from file doc-string
  • generalize dualPairing_nondegenerate + rename to id_nondegenerate
  • add accompanying id_separatingLeft, id_separatingRight and versions for Dual.eval (similar lemmas have also been proposed in #34487)

Estimated changes

modified theorem Module.dualPairing_apply