Commit 2022-01-15 09:16 ff19c951

View on Github →

chore(algebra/group_power/basic): collect together ring lemmas (#11446) This reorders the lemmas so that all the ring and comm_ring lemmas can be put in a single section.

Estimated changes

Modified src/algebra/group_power/basic.lean

modified theorem eq_or_eq_neg_of_sq_eq_sq

modified theorem mul_neg_one_pow_eq_zero_iff

modified theorem neg_one_pow_eq_or

modified theorem neg_one_pow_mul_eq_zero_iff

modified theorem neg_pow

modified theorem neg_pow_bit0

modified theorem neg_pow_bit1

modified theorem neg_sq

modified theorem of_mul_pow

modified theorem sq_sub_sq

modified theorem sub_sq