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
Scalar multiplication by naturals and integers is handled by the
notation defined elsewhere.
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.