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

See also the related negOnePow.

TODO

• Generalize this to Pow G (Zmod n) where orderOf g = n.

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 = ℤ.

instance instSMulZModOfNatNatAdditiveUnitsInt : SMul (ZMod 2) (Additive ℤˣ)

Equations

• instSMulZModOfNatNatAdditiveUnitsInt = { smul := fun (z : ZMod 2) (au : Additive ℤˣ) => Additive.ofMul (Additive.toMul au ^ z.val) }

theorem ZMod.smul_units_def (z : ZMod 2) (au : Additive ℤˣ) : z • au = z.val • au

theorem ZMod.natCast_smul_units (n : ℕ) (au : Additive ℤˣ) : ↑n • au = n • au

instance instModuleZModOfNatNatAdditiveUnitsInt : Module (ZMod 2) (Additive ℤˣ)

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

Equations

• instModuleZModOfNatNatAdditiveUnitsInt = Module.mk instModuleZModOfNatNatAdditiveUnitsInt.proof_5 instModuleZModOfNatNatAdditiveUnitsInt.proof_6

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) }

@[simp]

theorem ofMul_uzpow {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (u : ℤˣ) (r : R) : Additive.ofMul (u ^ r) = r • Additive.ofMul u

@[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

theorem uzpow_natCast {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (u : ℤˣ) (n : ℕ) : u ^ ↑n = u ^ n

theorem uzpow_coe_nat {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) (n : ℕ) [n.AtLeastTwo] : s ^ OfNat.ofNat n = s ^ OfNat.ofNat n

@[simp]

theorem one_uzpow {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (x : R) : 1 ^ x = 1

theorem mul_uzpow {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s₁ : ℤˣ) (s₂ : ℤˣ) (x : R) : (s₁ * s₂) ^ x = s₁ ^ x * s₂ ^ x

@[simp]

theorem uzpow_zero {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) : s ^ 0 = 1

@[simp]

theorem uzpow_one {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) : s ^ 1 = s

theorem uzpow_mul {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x : R) (y : R) : s ^ (x * y) = (s ^ x) ^ y

theorem uzpow_add {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x : R) (y : R) : s ^ (x + y) = s ^ x * s ^ y

theorem uzpow_sub {R : Type u_1} [CommRing R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x : R) (y : R) : s ^ (x - y) = s ^ x / s ^ y

theorem uzpow_neg {R : Type u_1} [CommRing R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x : R) : s ^ (-x) = (s ^ x)⁻¹

theorem uzpow_intCast {R : Type u_1} [CommRing R] [Module R (Additive ℤˣ)] (u : ℤˣ) (z : ℤ) : u ^ ↑z = u ^ z