cleanup: golf summable_prod_of_norm_coeff_le_linear #5

Activity

1. CBirkbeck

   added

   lane:cleanupWorker lane: /cleanup (golf/style; auto-merge)Worker lane: /cleanup (golf/style; auto-merge)

   state:todoTicket open, unclaimedTicket open, unclaimed

   state:in-progressTicket claimed + being workedTicket claimed + being worked

   and removed

   state:todoTicket open, unclaimedTicket open, unclaimed

   on Jun 17, 2026
2. CBirkbeck

   self-assigned this

   on Jun 17, 2026
3. CBirkbeck commented on Jun 17, 2026

   

   CBirkbeck

   on Jun 17, 2026

   OwnerAuthor

   More actions

   claimed
4. CBirkbeck commented on Jun 17, 2026

   

   CBirkbeck

   on Jun 17, 2026

   OwnerAuthor

   More actions

   Superseded by file-level cleanup tickets (whole-file granularity).
5. CBirkbeck

   closed this as completedon Jun 17, 2026
6. CBirkbeck commented on Jun 17, 2026

   

   CBirkbeck

   on Jun 17, 2026

   OwnerAuthor

   More actions

   Done via #264 (squash-merged). Acceptance bar green: lake build PadicLFunctions ✓, zero new sorry, #print axioms = [propext, Classical.choice, Quot.sound], statement byte-for-byte unchanged. Golf: gcongr for the hbd calc, by_contra!, inlined hn, dropped exfalso, stripped narrative comments. Body 40→33 lines.
7. CBirkbeck

   added a commit that references this issue on Jun 17, 2026

   cleanup: golf summable_prod_of_norm_coeff_le_linear (#5) (#264)

   ...

   180876f
8. CBirkbeck

   removed

   state:in-progressTicket claimed + being workedTicket claimed + being worked

   on Jun 17, 2026
9. CBirkbeck

   added a commit that references this issue on Jun 17, 2026

   cleanup: golf summable_prod_of_norm_coeff_le_linear (#5) (#264)

   ...

   e26a022
10. CBirkbeck

    added 2 commits that reference this issue on Jul 8, 2026

    board(T-H2b): core DONE (ForMathlib intertwining + baseChangeEquiv, a…

    ...

    2ac56cd

    docs(ModularCurves): T-UPSTREAM-TRIAGE — upstream-ledger.md (ranked, …

    ...

    464046f