Commit 2025-10-21 12:12 7702f1c6

View on Github →

chore(Algebra/Order/BigOperators/Group/List): remove commutativity assumptions (#30488)

Estimated changes

modified theorem List.monotone_prod_take
modified theorem List.prod_eq_one_iff