Lemmas about power operations on monoids and groups #
This file contains lemmas about Monoid.pow
, Group.pow
, nsmul
, and zsmul
which require additional imports besides those available in Mathlib.Algebra.GroupPower.Basic
.
(Additive) monoid #
Instances For
Instances For
Instances For
To show a property of all multiples of g
it suffices to show it is closed under
addition by g
and -g
on the left. For additive subgroups generated by more than one element, see
AddSubgroup.closure_induction_left
.
To show a property of all powers of g
it suffices to show it is closed under multiplication
by g
and g⁻¹
on the left. For subgroups generated by more than one element, see
Subgroup.closure_induction_left
.
To show a property of all multiples of g
it suffices to show it is closed under
addition by g
and -g
on the right. For additive subgroups generated by more than one element,
see AddSubgroup.closure_induction_right
.
To show a property of all powers of g
it suffices to show it is closed under multiplication
by g
and g⁻¹
on the right. For subgroups generated by more than one element, see
Subgroup.closure_induction_right
.
zpow
/zsmul
and an order #
Those lemmas are placed here
(rather than in Mathlib.Algebra.GroupPower.Order
with their friends)
because they require facts from Mathlib.Data.Int.Basic
.
See also smul_right_injective
. TODO: provide a NoZeroSMulDivisors
instance. We can't do
that here because importing that definition would create import cycles.
Alias of zsmul_right_inj
, for ease of discovery alongside
zsmul_le_zsmul_iff'
and zsmul_lt_zsmul_iff'
.
Alias of zsmul_right_inj
, for ease of discovery alongside zsmul_le_zsmul_iff'
and
zsmul_lt_zsmul_iff'
.
Note that AddCommMonoid.nat_smulCommClass
requires stronger assumptions on R
.
Note that AddCommMonoid.nat_isScalarTower
requires stronger assumptions on R
.
Note this holds in marginally more generality than Int.cast_mul
Note that AddCommGroup.int_smulCommClass
requires stronger assumptions on R
.
Note that AddCommGroup.int_isScalarTower
requires stronger assumptions on R
.
Alias of Int.natAbs_le_self_sq
.
Monoid homomorphisms from Multiplicative ℕ
are defined by the image
of Multiplicative.ofAdd 1
.
Instances For
Monoid homomorphisms from Multiplicative ℤ
are defined by the image
of Multiplicative.ofAdd 1
.
Instances For
MonoidHom.ext_mint
is defined in Data.Int.Cast
AddMonoidHom.ext_nat
is defined in Data.Nat.Cast
AddMonoidHom.ext_int
is defined in Data.Int.Cast
If M
is commutative, powersHom
is a multiplicative equivalence.
Instances For
If M
is commutative, zpowersHom
is a multiplicative equivalence.
Instances For
If M
is commutative, multiplesHom
is an additive equivalence.
Instances For
If M
is commutative, zmultiplesHom
is an additive equivalence.
Instances For
Commutativity (again) #
Facts about SemiconjBy
and Commute
that require zpow
or zsmul
, or the fact that integer
multiplication equals semiring multiplication.
Moving to the opposite monoid commutes with taking powers.
Moving to the opposite group or GroupWithZero
commutes with taking powers.