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

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

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.

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