Commit 2021-08-23 17:55 98a63294

refactor(algebra/group_power): use covariant_class (#8713)

Main changes

• use covariant_class instead of canonically_ordered_* or ordered_add_* as an assumption in many lemmas;
• move some lemmas to the root namespace;
• use to_additive for more lemmas;

Detailed list of API changes

• canonically_ordered_comm_semiring.pow_le_pow_of_le_left:
  • rename to pow_le_pow_of_le_left';
  • assume [covariant_class M M (*) (≤)];
  • use to_additive to generate nsmul_le_nsmul_of_le_right;
• canonically_ordered_comm_semiring.one_le_pow_of_one_le:
  • rename to one_le_pow_of_one_le';
  • assume [covariant_class M M (*) (≤)];
  • use to_additive to generate nsmul_nonneg;
• canonically_ordered_comm_semiring.pow_le_one:
  • rename to pow_le_one';
  • assume [covariant_class M M (*) (≤)];
  • use to_additive to generate nsmul_nonpos;
• add pow_le_pow', generate nsmul_le_nsmul;
• add pow_le_pow_of_le_one' and nsmul_le_nsmul_of_nonpos;
• add one_lt_pow', generate nsmul_pos;
  • as a side effect, nsmul_pos now assumes n ≠ 0 instead of 0 < n.
• add pow_lt_one', generate nsmul_neg;
• add pow_lt_pow', generate nsmul_lt_nsmul;
• generalize one_le_pow_iff and pow_le_one_iff, generate nsmul_nonneg_iff and nsmul_nonpos_iff;
• generalize one_lt_pow_iff, pow_lt_one_iff, and pow_eq_one_iff, generate nsmul_pos_iff, nsmul_neg_iff, and nsmul_eq_zero_iff;
• add one_le_gpow, generate gsmul_nonneg;
• rename eq_of_sq_eq_sq to sq_eq_sq, golf;
• drop eq_one_of_pow_eq_one in favor of the iff version pow_eq_one_iff;
• add missing instance nat.ordered_comm_semiring;

Misc changes

• replace some proofs about nat.pow with references to generic lemmas;
• add nnreal.coe_eq_one;