Commit 2020-10-04 03:45 e738e905

View on Github →

feat(algebra/group_power/identities): named ring identities (#4390) This PR adds a new file containing some "named" ring identities provable by ring.

Estimated changes

Created src/algebra/group_power/identities.lean

added theorem pow_four_add_four_mul_pow_four'

added theorem pow_four_add_four_mul_pow_four

added theorem pow_two_add_mul_pow_two_mul_pow_two_add_mul_pow_two

added theorem pow_two_add_pow_two_mul_pow_two_add_pow_two

added theorem sum_eight_sq_mul_sum_eight_sq

added theorem sum_four_sq_mul_sum_four_sq

Modified src/number_theory/sum_four_squares.lean