Repository navigation

feat: the conjugate of a Legendre function is Legendre [LS, Theorem 26.6] - #323

Open

prevostad wants to merge 3 commits into

LeanMachineLearning:mainfrom

prevostad:roadmap/legendre-conjugate-worker1

Open

feat: the conjugate of a Legendre function is Legendre [LS, Theorem 26.6]#323
prevostad wants to merge 3 commits into
LeanMachineLearning:mainfrom
prevostad:roadmap/legendre-conjugate-worker1

Commits on Nov 13, 2026
- feat: the conjugate of a Legendre function is Legendre [LS, Theorem 26.6]
  
  prevostad
  and
  web-flow
  committed
  bc5ae1d
- refactor: share the bidual-embedding facts in the Legendre conjugate proofs
  
  prevostad
  and
  web-flow
  committed
  5307124
- refactor: make the bidual-embedding facts public in a general file
  
  prevostad
  and
  web-flow
  committed
  3653de4