mathlib3

3d2fec5f - feat(algebra/group_power/basic): `pow_ne_zero_iff` and `pow_pos_iff` (#7307)

feat(algebra/group_power/basic): `pow_ne_zero_iff` and `pow_pos_iff` (#7307) For natural `n > 0`, - `a ^ n ≠ 0 ↔ a ≠ 0` - `0 < a ^ n ↔ 0 < a` where `a` is a member of a `linear_ordered_comm_monoid_with_zero`