Commit 2024-05-16 10:23 0f4f978f

View on Github →

chore: Move ring power lemmas earlier (#12818) After #12817, almost all lemmas can move from Algebra.GroupPower.Ring to earlier files at no cost. The few remaining lemmas could also move, but it would require a tiny bit more work.

Estimated changes

deleted theorem Ring.inverse_pow
deleted theorem add_sq'
deleted theorem add_sq
deleted theorem eq_or_eq_neg_of_sq_eq_sq
deleted theorem min_pow_dvd_add
deleted theorem neg_one_pow_eq_or
deleted theorem neg_one_sq
deleted theorem neg_pow'
deleted theorem neg_pow
deleted theorem neg_pow_bit0
deleted theorem neg_pow_bit1
deleted theorem neg_sq
deleted theorem sq_eq_one_iff
deleted theorem sq_eq_sq_iff_eq_or_eq_neg
deleted theorem sq_ne_one_iff
deleted theorem sq_sub_sq
deleted theorem sub_sq'
deleted theorem sub_sq
added theorem Ring.inverse_pow
added theorem neg_one_pow_eq_or
added theorem neg_one_sq
added theorem neg_pow'
added theorem neg_pow
added theorem neg_pow_bit0
added theorem neg_pow_bit1
added theorem neg_sq
added theorem sq_eq_one_iff
added theorem sq_ne_one_iff
added theorem sq_sub_sq
added theorem sub_sq'
added theorem sub_sq
added theorem add_sq'
added theorem add_sq
added theorem min_pow_dvd_add