Power operations on monoids and groups
The power operation on monoids and groups.
We separate this from group, because it depends on
which in turn depends on other parts of algebra.
We also define infix operators
•ℤ for scalar multiplication by a natural and an integer
We adopt the convention that
0^0 = 1.
This module provides the instance
has_pow ℕ ℕ (via
and is imported by
data.nat.basic, so it has to live low in the import hierarchy.
Not all of its imports are needed yet; the intent is to move more lemmas here from
so that they are available in
data.nat.basic, and the imports will be required then.