Commit 2026-08-15 23:59 bec97d68

View on Github →

chore(Algebra/BigOperators): add to_additive for expectation and antidiagonal lemmas (#42763)

  • Add @[to_additive] attributes to:
    • Expect.expect_inv_index
    • Nat.prod_antidiagonal_succ
    • Nat.prod_antidiagonal_succ'
  • Remove the duplicated additive proofs:
    • expect_neg_index
    • sum_antidiagonal_succ
    • sum_antidiagonal_succ' Used Aristotle AI to find the duplicates, and verify the change, and ChatGPT, AmazonQ to navigate VS Code, cli, running tests, making the PR, understanding the proof and so forth

Estimated changes

modified theorem Finset.expect_inv_index
deleted theorem Finset.expect_neg_index