Commit 2021-04-22 14:56 3d2fec5f
View on Github →feat(algebra/group_power/basic): pow_ne_zero_iff and pow_pos_iff (#7307)
For natural n > 0,
a ^ n ≠ 0 ↔ a ≠ 00 < a ^ n ↔ 0 < awhereais a member of alinear_ordered_comm_monoid_with_zero
feat(algebra/group_power/basic): pow_ne_zero_iff and pow_pos_iff (#7307)
For natural n > 0,
a ^ n ≠ 0 ↔ a ≠ 00 < a ^ n ↔ 0 < a where a is a member of a linear_ordered_comm_monoid_with_zero