Commit 2024-01-18 00:39 1e74fcff

View on Github →

feat(Algebra/CharP/{Basic|ExpChar}): add sum_pow_{char|expChar}_pow (#9799)

Estimated changes

Modified Mathlib/Algebra/CharP/Basic.lean

added theorem list_sum_pow_char_pow

added theorem multiset_sum_pow_char_pow

added theorem sum_pow_char_pow

Modified Mathlib/Algebra/CharP/ExpChar.lean

added theorem list_sum_pow_expChar

added theorem list_sum_pow_expChar_pow

added theorem multiset_sum_pow_expChar

added theorem multiset_sum_pow_expChar_pow

added theorem sum_pow_expChar

added theorem sum_pow_expChar_pow