mathlib3
ed5f6360 - chore(algebra/group_with_zero_power): review (#2966)

Commit
5 years ago
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.
Author
Parents
Loading