Documentation

Mathlib.Data.ZMod.Basic

Integers mod n #

Definition of the integers mod n, and the field structure on the integers mod p.

Definitions #

Equations
def ZMod.val {n : } :
ZMod n

val a is a natural number defined as:

  • for a : ZMod 0 it is the absolute value of a
  • for a : ZMod n with 0 < n it is the least natural number in the equivalence class

See ZMod.valMinAbs for a variant that takes values in the integers.

Equations
Instances For
    theorem ZMod.val_lt {n : } [NeZero n] (a : ZMod n) :
    theorem ZMod.val_le {n : } [NeZero n] (a : ZMod n) :
    @[simp]
    theorem ZMod.val_zero {n : } :
    @[simp]
    theorem ZMod.val_one' :
    @[simp]
    theorem ZMod.val_neg' {n : ZMod 0} :
    @[simp]
    theorem ZMod.val_mul' {m : ZMod 0} {n : ZMod 0} :
    @[simp]
    theorem ZMod.val_nat_cast {n : } (a : ) :
    ZMod.val a = a % n
    theorem ZMod.val_unit' {n : ZMod 0} :
    theorem ZMod.eq_one_of_isUnit_natCast {n : } (h : IsUnit n) :
    n = 1
    theorem ZMod.val_nat_cast_of_lt {n : } {a : } (h : a < n) :
    ZMod.val a = a
    instance ZMod.charP (n : ) :
    CharP (ZMod n) n
    Equations
    • =
    @[simp]
    theorem ZMod.addOrderOf_one (n : ) :
    @[simp]
    theorem ZMod.addOrderOf_coe (a : ) {n : } (n0 : n 0) :
    addOrderOf a = n / Nat.gcd n a

    This lemma works in the case in which ZMod n is not infinite, i.e. n ≠ 0. The version where a ≠ 0 is addOrderOf_coe'.

    @[simp]
    theorem ZMod.addOrderOf_coe' {a : } (n : ) (a0 : a 0) :
    addOrderOf a = n / Nat.gcd n a

    This lemma works in the case in which a ≠ 0. The version where ZMod n is not infinite, i.e. n ≠ 0, is addOrderOf_coe.

    theorem ZMod.ringChar_zmod_n (n : ) :

    We have that ringChar (ZMod n) = n.

    theorem ZMod.nat_cast_self (n : ) :
    n = 0
    @[simp]
    theorem ZMod.nat_cast_self' (n : ) :
    n + 1 = 0
    def ZMod.cast {R : Type u_1} [AddGroupWithOne R] {n : } :
    ZMod nR

    Cast an integer modulo n to another semiring. This function is a morphism if the characteristic of R divides n. See ZMod.castHom for a bundled version.

    Equations
    Instances For
      @[simp]
      theorem ZMod.cast_zero {n : } {R : Type u_1} [AddGroupWithOne R] :
      theorem ZMod.cast_eq_val {n : } {R : Type u_1} [AddGroupWithOne R] [NeZero n] (a : ZMod n) :
      @[simp]
      theorem Prod.fst_zmod_cast {n : } {R : Type u_1} [AddGroupWithOne R] {S : Type u_2} [AddGroupWithOne S] (a : ZMod n) :
      @[simp]
      theorem Prod.snd_zmod_cast {n : } {R : Type u_1} [AddGroupWithOne R] {S : Type u_2} [AddGroupWithOne S] (a : ZMod n) :
      theorem ZMod.nat_cast_zmod_val {n : } [NeZero n] (a : ZMod n) :
      (ZMod.val a) = a

      So-named because the coercion is Nat.cast into ZMod. For Nat.cast into an arbitrary ring, see ZMod.nat_cast_val.

      theorem ZMod.int_cast_zmod_cast {n : } (a : ZMod n) :
      (ZMod.cast a) = a

      So-named because the outer coercion is Int.cast into ZMod. For Int.cast into an arbitrary ring, see ZMod.int_cast_cast.

      theorem ZMod.cast_id (n : ) (i : ZMod n) :
      @[simp]
      theorem ZMod.cast_id' {n : } :
      ZMod.cast = id
      @[simp]
      theorem ZMod.nat_cast_comp_val {n : } (R : Type u_1) [Ring R] [NeZero n] :
      Nat.cast ZMod.val = ZMod.cast

      The coercions are respectively Nat.cast and ZMod.cast.

      @[simp]
      theorem ZMod.int_cast_comp_cast {n : } (R : Type u_1) [Ring R] :
      Int.cast ZMod.cast = ZMod.cast

      The coercions are respectively Int.cast, ZMod.cast, and ZMod.cast.

      @[simp]
      theorem ZMod.nat_cast_val {n : } {R : Type u_1} [Ring R] [NeZero n] (i : ZMod n) :
      @[simp]
      theorem ZMod.int_cast_cast {n : } {R : Type u_1} [Ring R] (i : ZMod n) :
      theorem ZMod.cast_add_eq_ite {n : } (a : ZMod n) (b : ZMod n) :
      ZMod.cast (a + b) = if n ZMod.cast a + ZMod.cast b then ZMod.cast a + ZMod.cast b - n else ZMod.cast a + ZMod.cast b

      If the characteristic of R divides n, then cast is a homomorphism.

      @[simp]
      theorem ZMod.cast_one {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) :
      theorem ZMod.cast_add {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (b : ZMod n) :
      theorem ZMod.cast_mul {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (b : ZMod n) :
      def ZMod.castHom {n : } {m : } (h : m n) (R : Type u_2) [Ring R] [CharP R m] :

      The canonical ring homomorphism from ZMod n to a ring of characteristic dividing n.

      See also ZMod.lift for a generalized version working in AddGroups.

      Equations
      • ZMod.castHom h R = { toMonoidHom := { toOneHom := { toFun := ZMod.cast, map_one' := }, map_mul' := }, map_zero' := , map_add' := }
      Instances For
        @[simp]
        theorem ZMod.castHom_apply {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] {h : m n} (i : ZMod n) :
        @[simp]
        theorem ZMod.cast_sub {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (b : ZMod n) :
        @[simp]
        theorem ZMod.cast_neg {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) :
        @[simp]
        theorem ZMod.cast_pow {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (k : ) :
        ZMod.cast (a ^ k) = ZMod.cast a ^ k
        @[simp]
        theorem ZMod.cast_nat_cast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
        ZMod.cast k = k
        @[simp]
        theorem ZMod.cast_int_cast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
        ZMod.cast k = k

        Some specialised simp lemmas which apply when R has characteristic n.

        @[simp]
        theorem ZMod.cast_one' {n : } {R : Type u_1} [Ring R] [CharP R n] :
        @[simp]
        theorem ZMod.cast_add' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
        @[simp]
        theorem ZMod.cast_mul' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
        @[simp]
        theorem ZMod.cast_sub' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
        @[simp]
        theorem ZMod.cast_pow' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (k : ) :
        ZMod.cast (a ^ k) = ZMod.cast a ^ k
        @[simp]
        theorem ZMod.cast_nat_cast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
        ZMod.cast k = k
        @[simp]
        theorem ZMod.cast_int_cast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
        ZMod.cast k = k
        theorem ZMod.castHom_injective {n : } (R : Type u_1) [Ring R] [CharP R n] :
        theorem ZMod.castHom_bijective {n : } (R : Type u_1) [Ring R] [CharP R n] [Fintype R] (h : Fintype.card R = n) :
        noncomputable def ZMod.ringEquiv {n : } (R : Type u_1) [Ring R] [CharP R n] [Fintype R] (h : Fintype.card R = n) :

        The unique ring isomorphism between ZMod n and a ring R of characteristic n and cardinality n.

        Equations
        Instances For
          def ZMod.ringEquivCongr {m : } {n : } (h : m = n) :

          The identity between ZMod m and ZMod n when m = n, as a ring isomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem ZMod.ringEquivCongr_trans {a : } {b : } {c : } (hab : a = b) (hbc : b = c) :
            theorem ZMod.ringEquivCongr_ringEquivCongr_apply {a : } {b : } {c : } (hab : a = b) (hbc : b = c) (x : ZMod a) :
            theorem ZMod.ringEquivCongr_val {a : } {b : } (h : a = b) (x : ZMod a) :
            theorem ZMod.int_coe_ringEquivCongr {a : } {b : } (h : a = b) (z : ) :
            (ZMod.ringEquivCongr h) z = z
            theorem ZMod.int_cast_eq_int_cast_iff (a : ) (b : ) (c : ) :
            a = b a b [ZMOD c]
            theorem ZMod.int_cast_eq_int_cast_iff' (a : ) (b : ) (c : ) :
            a = b a % c = b % c
            theorem ZMod.nat_cast_eq_nat_cast_iff (a : ) (b : ) (c : ) :
            a = b a b [MOD c]
            theorem ZMod.nat_cast_eq_nat_cast_iff' (a : ) (b : ) (c : ) :
            a = b a % c = b % c
            theorem ZMod.int_cast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
            a = 0 b a
            theorem ZMod.int_cast_eq_int_cast_iff_dvd_sub (a : ) (b : ) (c : ) :
            a = b c b - a
            theorem ZMod.nat_cast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
            a = 0 b a
            theorem ZMod.val_int_cast {n : } (a : ) [NeZero n] :
            (ZMod.val a) = a % n
            theorem ZMod.coe_int_cast {n : } (a : ) :
            ZMod.cast a = a % n
            @[simp]
            theorem ZMod.val_neg_one (n : ) :
            ZMod.val (-1) = n
            theorem ZMod.cast_neg_one {R : Type u_1} [Ring R] (n : ) :
            ZMod.cast (-1) = n - 1

            -1 : ZMod n lifts to n - 1 : R. This avoids the characteristic assumption in cast_neg.

            theorem ZMod.cast_sub_one {R : Type u_1} [Ring R] {n : } (k : ZMod n) :
            ZMod.cast (k - 1) = (if k = 0 then n else ZMod.cast k) - 1
            theorem ZMod.nat_coe_zmod_eq_iff (p : ) (n : ) (z : ZMod p) [NeZero p] :
            n = z ∃ (k : ), n = ZMod.val z + p * k
            theorem ZMod.int_coe_zmod_eq_iff (p : ) (n : ) (z : ZMod p) [NeZero p] :
            n = z ∃ (k : ), n = (ZMod.val z) + p * k
            @[simp]
            theorem ZMod.int_cast_mod (a : ) (b : ) :
            (a % b) = a
            theorem ZMod.cast_injective_of_le {m : } {n : } [nzm : NeZero m] (h : m n) :
            theorem ZMod.cast_zmod_eq_zero_iff_of_le {m : } {n : } [NeZero m] (h : m n) (a : ZMod m) :
            ZMod.cast a = 0 a = 0
            @[simp]
            theorem ZMod.nat_cast_toNat (p : ) {z : } (_h : 0 z) :
            (Int.toNat z) = z
            theorem ZMod.val_one (n : ) [Fact (1 < n)] :
            theorem ZMod.val_add {n : } [NeZero n] (a : ZMod n) (b : ZMod n) :
            ZMod.val (a + b) = (ZMod.val a + ZMod.val b) % n
            theorem ZMod.val_add_of_lt {n : } {a : ZMod n} {b : ZMod n} (h : ZMod.val a + ZMod.val b < n) :
            theorem ZMod.val_add_val_of_le {n : } [NeZero n] {a : ZMod n} {b : ZMod n} (h : n ZMod.val a + ZMod.val b) :
            theorem ZMod.val_add_of_le {n : } [NeZero n] {a : ZMod n} {b : ZMod n} (h : n ZMod.val a + ZMod.val b) :
            theorem ZMod.val_add_le {n : } (a : ZMod n) (b : ZMod n) :
            theorem ZMod.val_mul {n : } (a : ZMod n) (b : ZMod n) :
            theorem ZMod.val_mul_le {n : } (a : ZMod n) (b : ZMod n) :
            theorem ZMod.val_mul_of_lt {n : } {a : ZMod n} {b : ZMod n} (h : ZMod.val a * ZMod.val b < n) :
            instance ZMod.nontrivial (n : ) [Fact (1 < n)] :
            Equations
            • =
            def ZMod.inv (n : ) :
            ZMod nZMod n

            The inversion on ZMod n. It is setup in such a way that a * a⁻¹ is equal to gcd a.val n. In particular, if a is coprime to n, and hence a unit, a * a⁻¹ = 1.

            Equations
            Instances For
              instance ZMod.instInvZMod (n : ) :
              Inv (ZMod n)
              Equations
              theorem ZMod.inv_zero (n : ) :
              0⁻¹ = 0
              theorem ZMod.mul_inv_eq_gcd {n : } (a : ZMod n) :
              a * a⁻¹ = (Nat.gcd (ZMod.val a) n)
              @[simp]
              theorem ZMod.nat_cast_mod (a : ) (n : ) :
              (a % n) = a
              theorem ZMod.eq_iff_modEq_nat (n : ) {a : } {b : } :
              a = b a b [MOD n]
              theorem ZMod.coe_mul_inv_eq_one {n : } (x : ) (h : Nat.Coprime x n) :
              x * (x)⁻¹ = 1
              def ZMod.unitOfCoprime {n : } (x : ) (h : Nat.Coprime x n) :
              (ZMod n)ˣ

              unitOfCoprime makes an element of (ZMod n)ˣ given a natural number x and a proof that x is coprime to n

              Equations
              Instances For
                @[simp]
                theorem ZMod.coe_unitOfCoprime {n : } (x : ) (h : Nat.Coprime x n) :
                (ZMod.unitOfCoprime x h) = x
                theorem ZMod.isUnit_prime_iff_not_dvd {n : } {p : } (hp : Nat.Prime p) :
                IsUnit p ¬p n
                theorem ZMod.isUnit_prime_of_not_dvd {n : } {p : } (hp : Nat.Prime p) (h : ¬p n) :
                IsUnit p
                @[simp]
                theorem ZMod.inv_coe_unit {n : } (u : (ZMod n)ˣ) :
                (u)⁻¹ = u⁻¹
                theorem ZMod.mul_inv_of_unit {n : } (a : ZMod n) (h : IsUnit a) :
                a * a⁻¹ = 1
                theorem ZMod.inv_mul_of_unit {n : } (a : ZMod n) (h : IsUnit a) :
                a⁻¹ * a = 1
                theorem ZMod.inv_eq_of_mul_eq_one (n : ) (a : ZMod n) (b : ZMod n) (h : a * b = 1) :
                a⁻¹ = b
                def ZMod.unitsEquivCoprime {n : } [NeZero n] :
                (ZMod n)ˣ { x : ZMod n // Nat.Coprime (ZMod.val x) n }

                Equivalence between the units of ZMod n and the subtype of terms x : ZMod n for which x.val is coprime to n

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def ZMod.chineseRemainder {m : } {n : } (h : Nat.Coprime m n) :
                  ZMod (m * n) ≃+* ZMod m × ZMod n

                  The Chinese remainder theorem. For a pair of coprime natural numbers, m and n, the rings ZMod (m * n) and ZMod m × ZMod n are isomorphic.

                  See Ideal.quotientInfRingEquivPiQuotient for the Chinese remainder theorem for ideals in any ring.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem ZMod.add_self_eq_zero_iff_eq_zero {n : } (hn : Odd n) {a : ZMod n} :
                    a + a = 0 a = 0
                    theorem ZMod.ne_neg_self {n : } (hn : Odd n) {a : ZMod n} (ha : a 0) :
                    a -a
                    theorem ZMod.neg_one_ne_one {n : } [Fact (2 < n)] :
                    -1 1
                    @[simp]
                    theorem ZMod.natAbs_mod_two (a : ) :
                    (Int.natAbs a) = a
                    @[simp]
                    theorem ZMod.val_eq_zero {n : } (a : ZMod n) :
                    ZMod.val a = 0 a = 0
                    theorem ZMod.val_ne_zero {n : } (a : ZMod n) :
                    theorem ZMod.neg_eq_self_iff {n : } (a : ZMod n) :
                    -a = a a = 0 2 * ZMod.val a = n
                    theorem ZMod.val_cast_of_lt {n : } {a : } (h : a < n) :
                    ZMod.val a = a
                    theorem ZMod.neg_val' {n : } [NeZero n] (a : ZMod n) :
                    ZMod.val (-a) = (n - ZMod.val a) % n
                    theorem ZMod.neg_val {n : } [NeZero n] (a : ZMod n) :
                    ZMod.val (-a) = if a = 0 then 0 else n - ZMod.val a
                    theorem ZMod.val_neg_of_ne_zero {n : } [nz : NeZero n] (a : ZMod n) [na : NeZero a] :
                    theorem ZMod.val_sub {n : } [NeZero n] {a : ZMod n} {b : ZMod n} (h : ZMod.val b ZMod.val a) :
                    theorem ZMod.val_cast_eq_val_of_lt {m : } {n : } [nzm : NeZero m] {a : ZMod m} (h : ZMod.val a < n) :
                    theorem ZMod.cast_cast_zmod_of_le {m : } {n : } [hm : NeZero m] (h : m n) (a : ZMod m) :
                    def ZMod.valMinAbs {n : } :
                    ZMod n

                    valMinAbs x returns the integer in the same equivalence class as x that is closest to 0, The result will be in the interval (-n/2, n/2].

                    Equations
                    Instances For
                      @[simp]
                      theorem ZMod.valMinAbs_def_pos {n : } [NeZero n] (x : ZMod n) :
                      ZMod.valMinAbs x = if ZMod.val x n / 2 then (ZMod.val x) else (ZMod.val x) - n
                      @[simp]
                      theorem ZMod.coe_valMinAbs {n : } (x : ZMod n) :
                      (ZMod.valMinAbs x) = x
                      theorem Nat.le_div_two_iff_mul_two_le {n : } {m : } :
                      m n / 2 m * 2 n
                      theorem ZMod.valMinAbs_mem_Ioc {n : } [NeZero n] (x : ZMod n) :
                      ZMod.valMinAbs x * 2 Set.Ioc (-n) n
                      theorem ZMod.valMinAbs_spec {n : } [NeZero n] (x : ZMod n) (y : ) :
                      ZMod.valMinAbs x = y x = y y * 2 Set.Ioc (-n) n
                      @[simp]
                      @[simp]
                      theorem ZMod.valMinAbs_eq_zero {n : } (x : ZMod n) :
                      theorem ZMod.nat_cast_natAbs_valMinAbs {n : } [NeZero n] (a : ZMod n) :
                      (Int.natAbs (ZMod.valMinAbs a)) = if ZMod.val a n / 2 then a else -a
                      theorem ZMod.val_eq_ite_valMinAbs {n : } [NeZero n] (a : ZMod n) :
                      (ZMod.val a) = ZMod.valMinAbs a + (if ZMod.val a n / 2 then 0 else n)
                      theorem ZMod.prime_ne_zero (p : ) (q : ) [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p q) :
                      q 0
                      theorem ZMod.valMinAbs_natCast_of_le_half {n : } {a : } (ha : a n / 2) :
                      ZMod.valMinAbs a = a
                      theorem ZMod.valMinAbs_natCast_of_half_lt {n : } {a : } (ha : n / 2 < a) (ha' : a < n) :
                      ZMod.valMinAbs a = a - n
                      @[simp]
                      theorem ZMod.valMinAbs_natCast_eq_self {n : } {a : } [NeZero n] :
                      ZMod.valMinAbs a = a a n / 2
                      theorem ZMod.natAbs_min_of_le_div_two (n : ) (x : ) (y : ) (he : x = y) (hl : Int.natAbs x n / 2) :
                      instance ZMod.instFieldZMod (p : ) [Fact (Nat.Prime p)] :

                      Field structure on ZMod p if p is prime.

                      Equations
                      • One or more equations did not get rendered due to their size.

                      ZMod p is an integral domain when p is prime.

                      Equations
                      • =
                      theorem RingHom.ext_zmod {n : } {R : Type u_1} [Semiring R] (f : ZMod n →+* R) (g : ZMod n →+* R) :
                      f = g
                      instance ZMod.subsingleton_ringHom {n : } {R : Type u_1} [Semiring R] :
                      Equations
                      • =
                      instance ZMod.subsingleton_ringEquiv {n : } {R : Type u_1} [Semiring R] :
                      Equations
                      • =
                      @[simp]
                      theorem ZMod.ringHom_map_cast {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) (k : ZMod n) :
                      f (ZMod.cast k) = k
                      theorem ZMod.ringHom_rightInverse {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) :
                      Function.RightInverse ZMod.cast f
                      theorem ZMod.ringHom_surjective {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) :
                      theorem ZMod.ringHom_eq_of_ker_eq {n : } {R : Type u_1} [CommRing R] (f : R →+* ZMod n) (g : R →+* ZMod n) (h : RingHom.ker f = RingHom.ker g) :
                      f = g
                      @[simp]
                      @[simp]
                      theorem ZMod.castHom_comp {n : } {m : } {d : } (hm : n m) (hd : m d) :
                      def ZMod.lift (n : ) {A : Type u_2} [AddGroup A] :
                      { f : →+ A // f n = 0 } (ZMod n →+ A)

                      The map from ZMod n induced by f : ℤ →+ A that maps n to 0.

                      Equations
                      Instances For
                        @[simp]
                        theorem ZMod.lift_coe (n : ) {A : Type u_2} [AddGroup A] (f : { f : →+ A // f n = 0 }) (x : ) :
                        ((ZMod.lift n) f) x = f x
                        theorem ZMod.lift_castAddHom (n : ) {A : Type u_2} [AddGroup A] (f : { f : →+ A // f n = 0 }) (x : ) :
                        ((ZMod.lift n) f) ((Int.castAddHom (ZMod n)) x) = f x
                        @[simp]
                        theorem ZMod.lift_comp_coe (n : ) {A : Type u_2} [AddGroup A] (f : { f : →+ A // f n = 0 }) :
                        ((ZMod.lift n) f) Int.cast = f
                        @[simp]
                        theorem ZMod.lift_comp_castAddHom (n : ) {A : Type u_2} [AddGroup A] (f : { f : →+ A // f n = 0 }) :
                        theorem Nat.range_mul_add (m : ) (k : ) :
                        (Set.range fun (n : ) => m * n + k) = {n : | n = k k n}

                        The range of (m * · + k) on natural numbers is the set of elements ≥ k in the residue class of k mod m.