Commit 2020-09-25 00:12 f9a667d3
View on Github →refactor(algebra/group_power, data/nat/basic): remove redundant lemmas (#4243)
This removes lemmas about pow on nat which are redundant
with more general versions in the root namespace.
One notable removal is nat.pow_succ; use pow_succ' instead.
In order that the general versions are available already in data.nat.basic,
many lemmas from algebra.group_power.lemmas have been moved to
algebra.group_power.basic (basically as many as possible without adding imports).