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 #
Equations
- IsAddUnit.nsmul.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
Equations
- (_ : AddCommute x ((n - 1) • x)) = (_ : AddCommute x ((n - 1) • x))
If a natural multiple of x
is an additive unit, then x
is an additive unit.
Equations
- AddUnits.ofNSMul u x hn hu = AddUnits.leftOfAdd u x ((n - 1) • x) (_ : x + (n - 1) • x = ↑u) (_ : AddCommute x ((n - 1) • x))
Equations
- isAddUnit_nsmul_iff.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
If n • x = 0
, n ≠ 0≠ 0
, then x
is an additive unit.
Equations
- AddUnits.ofNSMulEqZero x n hx hn = AddUnits.ofNSMul 0 x hn hx
If x ^ n = 1
, n ≠ 0≠ 0
, then x
is a unit.
Equations
- Units.ofPowEqOne x n hx hn = Units.ofPow 1 x hn hx
If x ^ n = 1
then x
has an inverse, x^(n - 1)
.
Equations
- invertibleOfPowEqOne x n hx hn = Units.invertible (Units.ofPowEqOne x n hx hn)
Equations
- One or more equations did not get rendered due to their size.
Equations
- bit0_zsmul.match_1 motive x h_1 h_2 = Int.casesOn x (fun a => h_1 a) fun a => h_2 a
Equations
- add_one_zsmul.match_1 motive x h_1 h_2 h_3 = Int.casesOn x (fun a => h_1 a) fun a => Nat.casesOn a (h_2 ()) fun n => h_3 n
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 that AddCommGroup.int_smulCommClass
requires stronger assumptions on R
.
Note that AddCommGroup.int_isScalarTower
requires stronger assumptions on R
.
Bernoulli's inequality. This version works for semirings but requires
additional hypotheses 0 ≤ a * a≤ a * a
and 0 ≤ (1 + a) * (1 + a)≤ (1 + a) * (1 + a)
.
Alias of Int.natAbs_le_self_sq
.
Monoid homomorphisms from Multiplicative ℕ
are defined by the image
of Multiplicative.ofAdd 1
.
Equations
- powersHom M = Equiv.trans Additive.ofMul (Equiv.trans (multiplesHom (Additive M)) AddMonoidHom.toMultiplicative'')
Monoid homomorphisms from Multiplicative ℤ
are defined by the image
of Multiplicative.ofAdd 1
.
Equations
- zpowersHom G = Equiv.trans Additive.ofMul (Equiv.trans (zmultiplesHom (Additive G)) AddMonoidHom.toMultiplicative'')
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.
Equations
- One or more equations did not get rendered due to their size.
If M
is commutative, zpowersHom
is a multiplicative equivalence.
Equations
- One or more equations did not get rendered due to their size.
If M
is commutative, multiplesHom
is an additive equivalence.
Equations
- One or more equations did not get rendered due to their size.
If M
is commutative, zmultiplesHom
is an additive equivalence.
Equations
- One or more equations did not get rendered due to their size.
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 group or GroupWithZero
commutes with taking powers.