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 instSMulZModOfNatNatAdditiveUnitsInt :
SMul (ZMod 2) (Additive ℤˣ)
Equations
    source
    theorem ZMod.smul_units_def (z : ZMod 2) (au : Additive ℤˣ) :
    z • au = z.val • au
    source
    theorem ZMod.natCast_smul_units (n : ℕ) (au : Additive ℤˣ) :
    ↑n • au = n • au
    source
    instance instModuleZModOfNatNatAdditiveUnitsInt :
    Module (ZMod 2) (Additive ℤˣ)

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

    Equations
      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
        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 : ℕ) [n.AtLeastTwo] :
        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 y : R) :
        s ^ (x * y) = (s ^ x) ^ y
        source
        theorem uzpow_add {R : Type u_1} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x y : R) :
        s ^ (x + y) = s ^ x * s ^ y
        source
        theorem uzpow_sub {R : Type u_1} [CommRing R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x 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