Repository navigation

Split over-long proofs in PLAcceleratedNesterovLean - #757

Merged

Vilin97 merged 2 commits into

mainfrom

claude/split-long-proofs-placceleratednesterovlean

Nov 5, 2026

Merged

Split over-long proofs in PLAcceleratedNesterovLean#757
Vilin97 merged 2 commits into
mainfrom
claude/split-long-proofs-placceleratednesterovlean

Commits on Nov 5, 2026
- Split over-long proofs in PLAcceleratedNesterovLean
  
  Vilin97
  and
  claude
  committed
  26965ac
- Extract fderiv_kills_normal_of_eqOn from the local convergence proof
  
  Vilin97
  and
  claude
  committed
  3ce4c27