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.
This module contains the definitions of
and their additive counterparts
gsmul, along with a few lemmas.
Further lemmas can be found in
We also define infix operators
•ℤ for scalar multiplication by a natural and an integer
Implementation details #
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.