Commit 2026-08-31 10:08 cae66e9d

View on Github →

feat: add zero lemmas for even powers (#43161)

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

modified theorem Finset.sum_mul_self_eq_zero_iff

added theorem Finset.sum_pow_eq_zero_iff_of_even

added theorem Finset.sum_sq_eq_zero_iff

Modified Mathlib/Algebra/Order/Ring/Basic.lean

added theorem pow_add_pow_eq_zero_iff_of_even

Modified Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

modified theorem eq_zero_of_mul_self_add_mul_self_eq_zero

modified theorem mul_self_add_mul_self_eq_zero

added theorem sq_add_sq_eq_zero