Commit 2026-08-10 13:55 4a3cbc9c
View on Github →chore(Algebra/BigOperators): generate sum_Ico_reflect/sum_range_reflect with to_additive (#42592)
Tag prod_Ico_reflect/prod_range_reflect @[to_additive] and delete the hand-written twins.
Generated statements are identical.
I used Aristotle AI to find and solve these patterns