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) :
    a.val < n
    theorem ZMod.val_le {n : } [NeZero n] (a : ZMod n) :
    a.val n
    @[simp]
    theorem ZMod.val_zero {n : } :
    @[simp]
    theorem ZMod.val_one' :
    @[simp]
    theorem ZMod.val_neg' {n : ZMod 0} :
    (-n).val = n.val
    @[simp]
    theorem ZMod.val_mul' {m : ZMod 0} {n : ZMod 0} :
    (m * n).val = m.val * n.val
    @[simp]
    theorem ZMod.val_natCast {n : } (a : ) :
    (a).val = a % n
    @[deprecated ZMod.val_natCast]
    theorem ZMod.val_nat_cast {n : } (a : ) :
    (a).val = a % n

    Alias of ZMod.val_natCast.

    theorem ZMod.val_unit' {n : ZMod 0} :
    IsUnit n n.val = 1
    theorem ZMod.eq_one_of_isUnit_natCast {n : } (h : IsUnit n) :
    n = 1
    theorem ZMod.val_natCast_of_lt {n : } {a : } (h : a < n) :
    (a).val = a
    @[deprecated ZMod.val_natCast_of_lt]
    theorem ZMod.val_nat_cast_of_lt {n : } {a : } (h : a < n) :
    (a).val = a

    Alias of ZMod.val_natCast_of_lt.

    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 / n.gcd 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 / n.gcd 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.natCast_self (n : ) :
    n = 0
    @[deprecated ZMod.natCast_self]
    theorem ZMod.nat_cast_self (n : ) :
    n = 0

    Alias of ZMod.natCast_self.

    @[simp]
    theorem ZMod.natCast_self' (n : ) :
    n + 1 = 0
    @[deprecated ZMod.natCast_self']
    theorem ZMod.nat_cast_self' (n : ) :
    n + 1 = 0

    Alias of ZMod.natCast_self'.

    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
    • ZMod.cast = match (motive := (x : ) → ZMod xR) x with | 0 => Int.cast | n.succ => fun (i : ZMod (n + 1)) => i.val
    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) :
      a.cast = a.val
      @[simp]
      theorem Prod.fst_zmod_cast {n : } {R : Type u_1} [AddGroupWithOne R] {S : Type u_2} [AddGroupWithOne S] (a : ZMod n) :
      a.cast.1 = a.cast
      @[simp]
      theorem Prod.snd_zmod_cast {n : } {R : Type u_1} [AddGroupWithOne R] {S : Type u_2} [AddGroupWithOne S] (a : ZMod n) :
      a.cast.2 = a.cast
      theorem ZMod.natCast_zmod_val {n : } [NeZero n] (a : ZMod n) :
      a.val = a

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

      @[deprecated ZMod.natCast_zmod_val]
      theorem ZMod.nat_cast_zmod_val {n : } [NeZero n] (a : ZMod n) :
      a.val = a

      Alias of ZMod.natCast_zmod_val.


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

      @[deprecated ZMod.natCast_rightInverse]
      theorem ZMod.nat_cast_rightInverse {n : } [NeZero n] :
      Function.RightInverse ZMod.val Nat.cast

      Alias of ZMod.natCast_rightInverse.

      @[deprecated ZMod.natCast_zmod_surjective]

      Alias of ZMod.natCast_zmod_surjective.

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

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

      @[deprecated ZMod.intCast_zmod_cast]
      theorem ZMod.int_cast_zmod_cast {n : } (a : ZMod n) :
      a.cast = a

      Alias of ZMod.intCast_zmod_cast.


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

      @[deprecated ZMod.intCast_rightInverse]
      theorem ZMod.int_cast_rightInverse {n : } :
      Function.RightInverse ZMod.cast Int.cast

      Alias of ZMod.intCast_rightInverse.

      @[deprecated ZMod.intCast_surjective]

      Alias of ZMod.intCast_surjective.

      theorem ZMod.cast_id (n : ) (i : ZMod n) :
      i.cast = i
      @[simp]
      theorem ZMod.cast_id' {n : } :
      ZMod.cast = id
      @[simp]
      theorem ZMod.natCast_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.

      @[deprecated ZMod.natCast_comp_val]
      theorem ZMod.nat_cast_comp_val {n : } (R : Type u_1) [Ring R] [NeZero n] :
      Nat.cast ZMod.val = ZMod.cast

      Alias of ZMod.natCast_comp_val.


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

      @[simp]
      theorem ZMod.intCast_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.

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

      Alias of ZMod.intCast_comp_cast.


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

      @[simp]
      theorem ZMod.natCast_val {n : } {R : Type u_1} [Ring R] [NeZero n] (i : ZMod n) :
      i.val = i.cast
      @[deprecated ZMod.natCast_val]
      theorem ZMod.nat_cast_val {n : } {R : Type u_1} [Ring R] [NeZero n] (i : ZMod n) :
      i.val = i.cast

      Alias of ZMod.natCast_val.

      @[simp]
      theorem ZMod.intCast_cast {n : } {R : Type u_1} [Ring R] (i : ZMod n) :
      i.cast = i.cast
      @[deprecated ZMod.intCast_cast]
      theorem ZMod.int_cast_cast {n : } {R : Type u_1} [Ring R] (i : ZMod n) :
      i.cast = i.cast

      Alias of ZMod.intCast_cast.

      theorem ZMod.cast_add_eq_ite {n : } (a : ZMod n) (b : ZMod n) :
      (a + b).cast = if n a.cast + b.cast then a.cast + b.cast - n else a.cast + b.cast

      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) :
      (a + b).cast = a.cast + b.cast
      theorem ZMod.cast_mul {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (b : ZMod n) :
      (a * b).cast = a.cast * b.cast
      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 = { 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) :
        (ZMod.castHom h R) i = i.cast
        @[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) :
        (a - b).cast = a.cast - b.cast
        @[simp]
        theorem ZMod.cast_neg {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) :
        (-a).cast = -a.cast
        @[simp]
        theorem ZMod.cast_pow {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (k : ) :
        (a ^ k).cast = a.cast ^ k
        @[simp]
        theorem ZMod.cast_natCast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
        (k).cast = k
        @[deprecated ZMod.cast_natCast]
        theorem ZMod.cast_nat_cast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
        (k).cast = k

        Alias of ZMod.cast_natCast.

        @[simp]
        theorem ZMod.cast_intCast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
        (k).cast = k
        @[deprecated ZMod.cast_intCast]
        theorem ZMod.cast_int_cast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
        (k).cast = k

        Alias of ZMod.cast_intCast.

        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) :
        (a + b).cast = a.cast + b.cast
        @[simp]
        theorem ZMod.cast_mul' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
        (a * b).cast = a.cast * b.cast
        @[simp]
        theorem ZMod.cast_sub' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
        (a - b).cast = a.cast - b.cast
        @[simp]
        theorem ZMod.cast_pow' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (k : ) :
        (a ^ k).cast = a.cast ^ k
        @[simp]
        theorem ZMod.cast_natCast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
        (k).cast = k
        @[deprecated ZMod.cast_natCast']
        theorem ZMod.cast_nat_cast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
        (k).cast = k

        Alias of ZMod.cast_natCast'.

        @[simp]
        theorem ZMod.cast_intCast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
        (k).cast = k
        @[deprecated ZMod.cast_intCast']
        theorem ZMod.cast_int_cast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
        (k).cast = k

        Alias of ZMod.cast_intCast'.

        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
          noncomputable def ZMod.ringEquivOfPrime (R : Type u_1) [Ring R] [Fintype R] {p : } (hp : Nat.Prime p) (hR : Fintype.card R = p) :

          The unique ring isomorphism between ZMod p and a ring R of cardinality a prime p.

          If you need any property of this isomorphism, first of all use ringEquivOfPrime_eq_ringEquiv below (after have : CharP R p := ...) and deduce it by the results about ZMod.ringEquiv.

          Equations
          Instances For
            @[simp]
            theorem ZMod.ringEquivOfPrime_eq_ringEquiv (R : Type u_1) [Ring R] [Fintype R] {p : } [CharP R p] (hp : Nat.Prime p) (hR : Fintype.card R = p) :
            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_symm {a : } {b : } (hab : a = b) :
              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) :
              ((ZMod.ringEquivCongr h) x).val = x.val
              theorem ZMod.ringEquivCongr_intCast {a : } {b : } (h : a = b) (z : ) :
              (ZMod.ringEquivCongr h) z = z
              @[deprecated ZMod.ringEquivCongr_intCast]
              theorem ZMod.int_coe_ringEquivCongr {a : } {b : } (h : a = b) (z : ) :
              (ZMod.ringEquivCongr h) z = z

              Alias of ZMod.ringEquivCongr_intCast.

              theorem ZMod.intCast_eq_intCast_iff (a : ) (b : ) (c : ) :
              a = b a b [ZMOD c]
              @[deprecated ZMod.intCast_eq_intCast_iff]
              theorem ZMod.int_cast_eq_int_cast_iff (a : ) (b : ) (c : ) :
              a = b a b [ZMOD c]

              Alias of ZMod.intCast_eq_intCast_iff.

              theorem ZMod.intCast_eq_intCast_iff' (a : ) (b : ) (c : ) :
              a = b a % c = b % c
              @[deprecated ZMod.intCast_eq_intCast_iff']
              theorem ZMod.int_cast_eq_int_cast_iff' (a : ) (b : ) (c : ) :
              a = b a % c = b % c

              Alias of ZMod.intCast_eq_intCast_iff'.

              theorem ZMod.natCast_eq_natCast_iff (a : ) (b : ) (c : ) :
              a = b a b [MOD c]
              @[deprecated ZMod.natCast_eq_natCast_iff]
              theorem ZMod.nat_cast_eq_nat_cast_iff (a : ) (b : ) (c : ) :
              a = b a b [MOD c]

              Alias of ZMod.natCast_eq_natCast_iff.

              theorem ZMod.natCast_eq_natCast_iff' (a : ) (b : ) (c : ) :
              a = b a % c = b % c
              @[deprecated ZMod.natCast_eq_natCast_iff']
              theorem ZMod.nat_cast_eq_nat_cast_iff' (a : ) (b : ) (c : ) :
              a = b a % c = b % c

              Alias of ZMod.natCast_eq_natCast_iff'.

              theorem ZMod.intCast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
              a = 0 b a
              @[deprecated ZMod.intCast_zmod_eq_zero_iff_dvd]
              theorem ZMod.int_cast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
              a = 0 b a

              Alias of ZMod.intCast_zmod_eq_zero_iff_dvd.

              theorem ZMod.intCast_eq_intCast_iff_dvd_sub (a : ) (b : ) (c : ) :
              a = b c b - a
              @[deprecated ZMod.intCast_eq_intCast_iff_dvd_sub]
              theorem ZMod.int_cast_eq_int_cast_iff_dvd_sub (a : ) (b : ) (c : ) :
              a = b c b - a

              Alias of ZMod.intCast_eq_intCast_iff_dvd_sub.

              theorem ZMod.natCast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
              a = 0 b a
              @[deprecated ZMod.natCast_zmod_eq_zero_iff_dvd]
              theorem ZMod.nat_cast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
              a = 0 b a

              Alias of ZMod.natCast_zmod_eq_zero_iff_dvd.

              theorem ZMod.val_intCast {n : } (a : ) [NeZero n] :
              (a).val = a % n
              @[deprecated ZMod.val_intCast]
              theorem ZMod.val_int_cast {n : } (a : ) [NeZero n] :
              (a).val = a % n

              Alias of ZMod.val_intCast.

              theorem ZMod.coe_intCast {n : } (a : ) :
              (a).cast = a % n
              @[deprecated ZMod.coe_intCast]
              theorem ZMod.coe_int_cast {n : } (a : ) :
              (a).cast = a % n

              Alias of ZMod.coe_intCast.

              theorem ZMod.intCast_cast_add {n : } (x : ZMod n) (y : ZMod n) :
              (x + y).cast = (x.cast + y.cast) % n
              theorem ZMod.intCast_cast_mul {n : } (x : ZMod n) (y : ZMod n) :
              (x * y).cast = x.cast * y.cast % n
              theorem ZMod.intCast_cast_sub {n : } (x : ZMod n) (y : ZMod n) :
              (x - y).cast = (x.cast - y.cast) % n
              theorem ZMod.intCast_cast_neg {n : } (x : ZMod n) :
              (-x).cast = -x.cast % n
              @[simp]
              theorem ZMod.val_neg_one (n : ) :
              (-1).val = n
              theorem ZMod.cast_neg_one {R : Type u_1} [Ring R] (n : ) :
              (-1).cast = 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) :
              (k - 1).cast = (if k = 0 then n else k.cast) - 1
              theorem ZMod.natCast_eq_iff (p : ) (n : ) (z : ZMod p) [NeZero p] :
              n = z ∃ (k : ), n = z.val + p * k
              theorem ZMod.intCast_eq_iff (p : ) (n : ) (z : ZMod p) [NeZero p] :
              n = z ∃ (k : ), n = z.val + p * k
              @[deprecated ZMod.natCast_eq_iff]
              theorem ZMod.nat_coe_zmod_eq_iff (p : ) (n : ) (z : ZMod p) [NeZero p] :
              n = z ∃ (k : ), n = z.val + p * k

              Alias of ZMod.natCast_eq_iff.

              @[deprecated ZMod.intCast_eq_iff]
              theorem ZMod.int_coe_zmod_eq_iff (p : ) (n : ) (z : ZMod p) [NeZero p] :
              n = z ∃ (k : ), n = z.val + p * k

              Alias of ZMod.intCast_eq_iff.

              @[simp]
              theorem ZMod.intCast_mod (a : ) (b : ) :
              (a % b) = a
              @[deprecated ZMod.intCast_mod]
              theorem ZMod.int_cast_mod (a : ) (b : ) :
              (a % b) = a

              Alias of ZMod.intCast_mod.

              @[deprecated ZMod.ker_intCastAddHom]

              Alias of ZMod.ker_intCastAddHom.

              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) :
              a.cast = 0 a = 0
              @[simp]
              theorem ZMod.natCast_toNat (p : ) {z : } (_h : 0 z) :
              z.toNat = z
              @[deprecated ZMod.natCast_toNat]
              theorem ZMod.nat_cast_toNat (p : ) {z : } (_h : 0 z) :
              z.toNat = z

              Alias of ZMod.natCast_toNat.

              theorem ZMod.val_one (n : ) [Fact (1 < n)] :
              theorem ZMod.val_one'' {n : } :
              n 1ZMod.val 1 = 1
              theorem ZMod.val_add {n : } [NeZero n] (a : ZMod n) (b : ZMod n) :
              (a + b).val = (a.val + b.val) % n
              theorem ZMod.val_add_of_lt {n : } {a : ZMod n} {b : ZMod n} (h : a.val + b.val < n) :
              (a + b).val = a.val + b.val
              theorem ZMod.val_add_val_of_le {n : } [NeZero n] {a : ZMod n} {b : ZMod n} (h : n a.val + b.val) :
              a.val + b.val = (a + b).val + n
              theorem ZMod.val_add_of_le {n : } [NeZero n] {a : ZMod n} {b : ZMod n} (h : n a.val + b.val) :
              (a + b).val = a.val + b.val - n
              theorem ZMod.val_add_le {n : } (a : ZMod n) (b : ZMod n) :
              (a + b).val a.val + b.val
              theorem ZMod.val_mul {n : } (a : ZMod n) (b : ZMod n) :
              (a * b).val = a.val * b.val % n
              theorem ZMod.val_mul_le {n : } (a : ZMod n) (b : ZMod n) :
              (a * b).val a.val * b.val
              theorem ZMod.val_mul_of_lt {n : } {a : ZMod n} {b : ZMod n} (h : a.val * b.val < n) :
              (a * b).val = a.val * b.val
              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
              • ZMod.inv x✝ x = match x✝, x with | 0, i => Int.sign i | n.succ, i => (i.val.gcdA (n + 1))
              Instances For
                instance ZMod.instInv (n : ) :
                Inv (ZMod n)
                Equations
                theorem ZMod.inv_zero (n : ) :
                0⁻¹ = 0
                theorem ZMod.mul_inv_eq_gcd {n : } (a : ZMod n) :
                a * a⁻¹ = (a.val.gcd n)
                @[simp]
                theorem ZMod.inv_one (n : ) :
                1⁻¹ = 1
                @[simp]
                theorem ZMod.natCast_mod (a : ) (n : ) :
                (a % n) = a
                @[deprecated ZMod.natCast_mod]
                theorem ZMod.nat_cast_mod (a : ) (n : ) :
                (a % n) = a

                Alias of ZMod.natCast_mod.

                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 : x.Coprime n) :
                x * (x)⁻¹ = 1
                theorem ZMod.mul_val_inv {m : } {n : } (hmn : m.Coprime n) :
                m * (m)⁻¹.val = 1
                theorem ZMod.val_inv_mul {m : } {n : } (hmn : m.Coprime n) :
                (m)⁻¹.val * m = 1
                def ZMod.unitOfCoprime {n : } (x : ) (h : x.Coprime 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 : x.Coprime n) :
                  (ZMod.unitOfCoprime x h) = x
                  theorem ZMod.val_coe_unit_coprime {n : } (u : (ZMod n)ˣ) :
                  (u).val.Coprime n
                  theorem ZMod.isUnit_iff_coprime (m : ) (n : ) :
                  IsUnit m m.Coprime n
                  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 // x.val.Coprime 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
                  • ZMod.unitsEquivCoprime = { toFun := fun (x : (ZMod n)ˣ) => x, , invFun := fun (x : { x : ZMod n // x.val.Coprime n }) => ZMod.unitOfCoprime (x).val , left_inv := , right_inv := }
                  Instances For
                    def ZMod.chineseRemainder {m : } {n : } (h : m.Coprime 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 : ) :
                      a.natAbs = a
                      @[simp]
                      theorem ZMod.val_eq_zero {n : } (a : ZMod n) :
                      a.val = 0 a = 0
                      theorem ZMod.val_ne_zero {n : } (a : ZMod n) :
                      a.val 0 a 0
                      theorem ZMod.neg_eq_self_iff {n : } (a : ZMod n) :
                      -a = a a = 0 2 * a.val = n
                      theorem ZMod.val_cast_of_lt {n : } {a : } (h : a < n) :
                      (a).val = a
                      theorem ZMod.neg_val' {n : } [NeZero n] (a : ZMod n) :
                      (-a).val = (n - a.val) % n
                      theorem ZMod.neg_val {n : } [NeZero n] (a : ZMod n) :
                      (-a).val = if a = 0 then 0 else n - a.val
                      theorem ZMod.val_neg_of_ne_zero {n : } [nz : NeZero n] (a : ZMod n) [na : NeZero a] :
                      (-a).val = n - a.val
                      theorem ZMod.val_sub {n : } [NeZero n] {a : ZMod n} {b : ZMod n} (h : b.val a.val) :
                      (a - b).val = a.val - b.val
                      theorem ZMod.val_cast_eq_val_of_lt {m : } {n : } [nzm : NeZero m] {a : ZMod m} (h : a.val < n) :
                      a.cast.val = a.val
                      theorem ZMod.cast_cast_zmod_of_le {m : } {n : } [hm : NeZero m] (h : m n) (a : ZMod m) :
                      a.cast.cast = a
                      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
                      • x.valMinAbs = match x✝, x with | 0, x => x | n@h:n_1.succ, x => if x.val n / 2 then x.val else x.val - n
                      Instances For
                        @[simp]
                        theorem ZMod.valMinAbs_def_zero (x : ZMod 0) :
                        x.valMinAbs = x
                        theorem ZMod.valMinAbs_def_pos {n : } [NeZero n] (x : ZMod n) :
                        x.valMinAbs = if x.val n / 2 then x.val else x.val - n
                        @[simp]
                        theorem ZMod.coe_valMinAbs {n : } (x : ZMod n) :
                        x.valMinAbs = x
                        theorem Nat.le_div_two_iff_mul_two_le {n : } {m : } :
                        m n / 2 m * 2 n
                        theorem ZMod.valMinAbs_nonneg_iff {n : } [NeZero n] (x : ZMod n) :
                        0 x.valMinAbs x.val n / 2
                        theorem ZMod.valMinAbs_mul_two_eq_iff {n : } (a : ZMod n) :
                        a.valMinAbs * 2 = n 2 * a.val = n
                        theorem ZMod.valMinAbs_mem_Ioc {n : } [NeZero n] (x : ZMod n) :
                        x.valMinAbs * 2 Set.Ioc (-n) n
                        theorem ZMod.valMinAbs_spec {n : } [NeZero n] (x : ZMod n) (y : ) :
                        x.valMinAbs = y x = y y * 2 Set.Ioc (-n) n
                        theorem ZMod.natAbs_valMinAbs_le {n : } [NeZero n] (x : ZMod n) :
                        x.valMinAbs.natAbs n / 2
                        @[simp]
                        @[simp]
                        theorem ZMod.valMinAbs_eq_zero {n : } (x : ZMod n) :
                        x.valMinAbs = 0 x = 0
                        theorem ZMod.natCast_natAbs_valMinAbs {n : } [NeZero n] (a : ZMod n) :
                        a.valMinAbs.natAbs = if a.val n / 2 then a else -a
                        @[deprecated ZMod.natCast_natAbs_valMinAbs]
                        theorem ZMod.nat_cast_natAbs_valMinAbs {n : } [NeZero n] (a : ZMod n) :
                        a.valMinAbs.natAbs = if a.val n / 2 then a else -a

                        Alias of ZMod.natCast_natAbs_valMinAbs.

                        theorem ZMod.valMinAbs_neg_of_ne_half {n : } {a : ZMod n} (ha : 2 * a.val n) :
                        (-a).valMinAbs = -a.valMinAbs
                        @[simp]
                        theorem ZMod.natAbs_valMinAbs_neg {n : } (a : ZMod n) :
                        (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
                        theorem ZMod.val_eq_ite_valMinAbs {n : } [NeZero n] (a : ZMod n) :
                        a.val = a.valMinAbs + (if a.val 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_natAbs_eq_min {n : } [hpos : NeZero n] (a : ZMod n) :
                        a.valMinAbs.natAbs = min a.val (n - a.val)
                        theorem ZMod.valMinAbs_natCast_of_le_half {n : } {a : } (ha : a n / 2) :
                        (a).valMinAbs = a
                        theorem ZMod.valMinAbs_natCast_of_half_lt {n : } {a : } (ha : n / 2 < a) (ha' : a < n) :
                        (a).valMinAbs = a - n
                        @[simp]
                        theorem ZMod.valMinAbs_natCast_eq_self {n : } {a : } [NeZero n] :
                        (a).valMinAbs = a a n / 2
                        theorem ZMod.natAbs_min_of_le_div_two (n : ) (x : ) (y : ) (he : x = y) (hl : x.natAbs n / 2) :
                        x.natAbs y.natAbs
                        theorem ZMod.natAbs_valMinAbs_add_le {n : } (a : ZMod n) (b : ZMod n) :
                        (a + b).valMinAbs.natAbs (a.valMinAbs + b.valMinAbs).natAbs
                        instance ZMod.instField (p : ) [Fact (Nat.Prime p)] :

                        Field structure on ZMod p if p is prime.

                        Equations
                        instance ZMod.instIsDomain (p : ) [hp : Fact (Nat.Prime p)] :

                        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 k.cast = k
                        theorem ZMod.ringHom_rightInverse {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) :
                        Function.RightInverse ZMod.cast f

                        Any ring homomorphism into ZMod n has a right inverse.

                        theorem ZMod.ringHom_surjective {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) :

                        Any ring homomorphism into ZMod n is surjective.

                        @[simp]
                        @[simp]
                        theorem ZMod.castHom_comp {n : } {m : } {d : } (hm : n m) (hd : m d) :
                        (ZMod.castHom hm (ZMod n)).comp (ZMod.castHom hd (ZMod m)) = ZMod.castHom (ZMod n)
                        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 }) :
                          ((ZMod.lift n) f).comp (Int.castAddHom (ZMod n)) = f
                          theorem ZMod.lift_injective (n : ) {A : Type u_2} [AddGroup A] {f : { f : →+ A // f n = 0 }} :
                          Function.Injective ((ZMod.lift n) f) ∀ (m : ), f m = 0m = 0
                          @[simp]
                          theorem nsmul_zmod_val_inv_nsmul {α : Type u_1} [AddGroup α] {n : } (hn : (Nat.card α).Coprime n) (a : α) :
                          n (n)⁻¹.val a = a
                          @[simp]
                          theorem zmod_val_inv_nsmul_nsmul {α : Type u_1} [AddGroup α] {n : } (hn : (Nat.card α).Coprime n) (a : α) :
                          (n)⁻¹.val n a = a
                          @[simp]
                          theorem pow_zmod_val_inv_pow {α : Type u_1} [Group α] {n : } (hn : (Nat.card α).Coprime n) (a : α) :
                          (a ^ (n)⁻¹.val) ^ n = a
                          @[simp]
                          theorem pow_pow_zmod_val_inv {α : Type u_1} [Group α] {n : } (hn : (Nat.card α).Coprime n) (a : α) :
                          (a ^ n) ^ (n)⁻¹.val = a
                          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.