Commit 2022-05-31 20:07 9dc4b8ec

feat(algebra/group_power/basic): a^2 = b^2 ↔ a = b ∨ a = -b (#14431) Generalize a ^ 2 = 1 ↔ a = 1 ∨ a = -1 to ring + no_zero_divisors and prove a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b under comm_ring + no_zero_divisors.