Documentation

Mathlib.Data.ZMod.IntUnitsPower

The power operator on ℤˣ by ZMod 2, ℕ, and ℤ #

See also the related negOnePow.

TODO #

Implementation notes #

In future, we could consider a LawfulPower M R typeclass; but we can save ourselves a lot of work by using Module R (Additive M) in its place, especially since this already has instances for R = ℕ and R = ℤ.

source
instance instSMulZModOfNatNatInstOfNatNatAdditiveUnitsIntInstMonoidInt :
SMul (ZMod 2) (Additive ℤˣ)
Equations
source
theorem ZMod.smul_units_def (z : ZMod 2) (au : Additive ℤˣ) :
z • au = ZMod.val z • au
source
theorem ZMod.natCast_smul_units (n : ℕ) (au : Additive ℤˣ) :
↑n • au = n • au
source
instance instModuleZModOfNatNatInstOfNatNatAdditiveUnitsIntInstMonoidIntToSemiringToDivisionSemiringToSemifieldInstFieldZModFact_prime_twoAddCommMonoidToCommMonoidInstCommGroupUnitsInstCommMonoidInt :
Module (ZMod 2) (Additive ℤˣ)

This is an indirect way of saying that ℤˣ has a power operation by ZMod 2.

Equations
  • One or more equations did not get rendered due to their size.
source
instance Int.instUnitsPow {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] :
Pow ℤˣ R

There is a canonical power operation on ℤˣ by R if Additive ℤˣ is an R-module.

In lemma names, this operations is called uzpow to match zpow.

Notably this is satisfied by R ∈ {ℕ, ℤ, ZMod 2}.

Equations
  • Int.instUnitsPow = { pow := fun (u : ℤˣ) (r : R) => Additive.toMul (r • Additive.ofMul u) }
source
@[simp]
theorem ofMul_uzpow {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (u : ℤˣ) (r : R) :
Additive.ofMul (u ^ r) = r • Additive.ofMul u
source
@[simp]
theorem toMul_uzpow {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (u : Additive ℤˣ) (r : R) :
Additive.toMul (r • u) = Additive.toMul u ^ r
source
theorem uzpow_natCast {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (u : ℤˣ) (n : ℕ) :
u ^ ↑n = u ^ n
source
theorem uzpow_coe_nat {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) (n : ℕ) [Nat.AtLeastTwo n] :
s ^ OfNat.ofNat n = s ^ OfNat.ofNat n
source
@[simp]
theorem one_uzpow {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (x : R) :
1 ^ x = 1
source
theorem mul_uzpow {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s₁ : ℤˣ) (s₂ : ℤˣ) (x : R) :
(s₁ * s₂) ^ x = s₁ ^ x * s₂ ^ x
source
@[simp]
theorem uzpow_zero {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) :
s ^ 0 = 1
source
@[simp]
theorem uzpow_one {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) :
s ^ 1 = s
source
theorem uzpow_mul {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x : R) (y : R) :
s ^ (x * y) = (s ^ x) ^ y
source
theorem uzpow_add {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x : R) (y : R) :
s ^ (x + y) = s ^ x * s ^ y
source
theorem uzpow_sub {R : Type u_1} [CommRing R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x : R) (y : R) :
s ^ (x - y) = s ^ x / s ^ y
source
theorem uzpow_neg {R : Type u_1} [CommRing R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x : R) :
s ^ (-x) = (s ^ x)⁻¹
source
theorem uzpow_intCast {R : Type u_1} [CommRing R] [Module R (Additive ℤˣ)] (u : ℤˣ) (z : ℤ) :
u ^ ↑z = u ^ z