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

Equations
theorem ZMod.smul_units_def (z : ZMod 2) (au : ) :
z au = z.val au
theorem ZMod.natCast_smul_units (n : ) (au : ) :
n au = n au

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

Equations
instance Int.instUnitsPow {R : Type u_1} [] [Module 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} [] [Module R ] (u : ) (r : R) :
@[simp]
theorem toMul_uzpow {R : Type u_1} [] [Module R ] (u : ) (r : R) :
theorem uzpow_natCast {R : Type u_1} [] [Module R ] (u : ) (n : ) :
u ^ n = u ^ n
theorem uzpow_coe_nat {R : Type u_1} [] [Module R ] (s : ) (n : ) [n.AtLeastTwo] :
s ^ = s ^
@[simp]
theorem one_uzpow {R : Type u_1} [] [Module R ] (x : R) :
1 ^ x = 1
theorem mul_uzpow {R : Type u_1} [] [Module R ] (s₁ : ) (s₂ : ) (x : R) :
(s₁ * s₂) ^ x = s₁ ^ x * s₂ ^ x
@[simp]
theorem uzpow_zero {R : Type u_1} [] [Module R ] (s : ) :
s ^ 0 = 1
@[simp]
theorem uzpow_one {R : Type u_1} [] [Module R ] (s : ) :
s ^ 1 = s
theorem uzpow_mul {R : Type u_1} [] [Module R ] (s : ) (x : R) (y : R) :
s ^ (x * y) = (s ^ x) ^ y
theorem uzpow_add {R : Type u_1} [] [Module R ] (s : ) (x : R) (y : R) :
s ^ (x + y) = s ^ x * s ^ y
theorem uzpow_sub {R : Type u_1} [] [Module R ] (s : ) (x : R) (y : R) :
s ^ (x - y) = s ^ x / s ^ y
theorem uzpow_neg {R : Type u_1} [] [Module R ] (s : ) (x : R) :
s ^ (-x) = (s ^ x)⁻¹
theorem uzpow_intCast {R : Type u_1} [] [Module R ] (u : ) (z : ) :
u ^ z = u ^ z