Commit 2020-06-06 15:39 ed5f6360

chore(algebra/group_with_zero_power): review (#2966) List of changes:

• Rename gpow_neg_succ to gpow_neg_succ_of_nat to match other names in int namespace.
• Add units.coe_gpow.
• Remove fpow_neg_succ, leave fpow_neg_succ_of_nat.
• Rewrite the proof of fpow_add in the same way I rewrote the proof of gpow_add.
• Make argument a implicit in some lemmas because they have an argument ha : a ≠ 0.
• Remove fpow_inv. This was a copy of fpow_neg_one with a misleading name.
• Remove unit_pow in favor of a more general units.coe_pow.
• Remove unit_gpow, add a more general units.coe_gpow' instead.