Documentation

Mathlib.Data.ZMod.Basic

Integers mod n #

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

Definitions #

def ZMod.finEquiv (n : ) [NeZero n] :

For non-zero n : ℕ, the ring Fin n is equivalent to ZMod n.

Equations
    Instances For
      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 : } :
          val 0 = 0
          @[simp]
          theorem ZMod.val_one' :
          val 1 = 1
          @[simp]
          theorem ZMod.val_neg' {n : ZMod 0} :
          (-n).val = n.val
          @[simp]
          theorem ZMod.val_mul' {m n : ZMod 0} :
          (m * n).val = m.val * n.val
          @[simp]
          theorem ZMod.val_natCast (n a : ) :
          (↑a).val = a % n
          theorem ZMod.val_natCast_of_lt {n a : } (h : a < n) :
          (↑a).val = a
          theorem ZMod.val_ofNat_of_lt {n a : } [a.AtLeastTwo] (han : a < n) :
          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
          instance ZMod.charP (n : ) :
          CharP (ZMod n) n
          @[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
          @[simp]
          theorem ZMod.natCast_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] :
              cast 0 = 0
              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.

              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.

              theorem ZMod.forall {n : } {P : ZMod nProp} :
              (∀ (x : ZMod n), P x) ∀ (x : ), P x
              theorem ZMod.exists {n : } {P : ZMod nProp} :
              (∃ (x : ZMod n), P x) ∃ (x : ), P x
              theorem ZMod.cast_id (n : ) (i : ZMod n) :
              i.cast = i
              @[simp]
              theorem ZMod.cast_id' {n : } :
              @[simp]
              theorem ZMod.natCast_comp_val {n : } (R : Type u_1) [Ring R] [NeZero n] :

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

              @[simp]
              theorem ZMod.intCast_comp_cast {n : } (R : Type u_1) [Ring R] :

              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
              @[simp]
              theorem ZMod.intCast_cast {n : } {R : Type u_1} [Ring R] (i : ZMod n) :
              i.cast = i.cast
              theorem ZMod.cast_add_eq_ite {n : } (a 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) :
              cast 1 = 1
              @[simp]
              theorem ZMod.cast_add {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a b : ZMod n) :
              (a + b).cast = a.cast + b.cast
              @[simp]
              theorem ZMod.cast_mul {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a 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
                Instances For
                  @[simp]
                  theorem ZMod.castHom_apply {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] {h : m n} (i : ZMod n) :
                  (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 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
                  @[simp]
                  theorem ZMod.cast_intCast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
                  (↑k).cast = k

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

                  theorem ZMod.cast_one' {n : } {R : Type u_1} [Ring R] [CharP R n] :
                  cast 1 = 1
                  theorem ZMod.cast_add' {n : } {R : Type u_1} [Ring R] [CharP R n] (a b : ZMod n) :
                  (a + b).cast = a.cast + b.cast
                  theorem ZMod.cast_mul' {n : } {R : Type u_1} [Ring R] [CharP R n] (a b : ZMod n) :
                  (a * b).cast = a.cast * b.cast
                  theorem ZMod.cast_sub' {n : } {R : Type u_1} [Ring R] [CharP R n] (a b : ZMod n) :
                  (a - b).cast = a.cast - b.cast
                  theorem ZMod.cast_pow' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (k : ) :
                  (a ^ k).cast = a.cast ^ k
                  theorem ZMod.cast_natCast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
                  (↑k).cast = k
                  theorem ZMod.cast_intCast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
                  (↑k).cast = 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
                      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
                            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) :
                              theorem ZMod.ringEquivCongr_intCast {a b : } (h : a = b) (z : ) :
                              (ringEquivCongr h) z = z
                              @[simp]
                              theorem ZMod.val_eq_zero {n : } (a : ZMod n) :
                              a.val = 0 a = 0
                              theorem ZMod.intCast_eq_intCast_iff (a b : ) (c : ) :
                              a = b a b [ZMOD c]
                              theorem ZMod.intCast_eq_intCast_iff' (a b : ) (c : ) :
                              a = b a % c = b % c
                              theorem ZMod.val_intCast {n : } (a : ) [NeZero n] :
                              (↑a).val = a % n
                              theorem ZMod.natCast_eq_natCast_iff (a b c : ) :
                              a = b a b [MOD c]
                              theorem ZMod.natCast_eq_natCast_iff' (a b c : ) :
                              a = b a % c = b % c
                              theorem ZMod.intCast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
                              a = 0 b a
                              theorem ZMod.intCast_eq_intCast_iff_dvd_sub (a b : ) (c : ) :
                              a = b c b - a
                              theorem ZMod.coe_intCast {n : } (a : ) :
                              (↑a).cast = a % n
                              theorem ZMod.intCast_cast_add {n : } (x y : ZMod n) :
                              (x + y).cast = (x.cast + y.cast) % n
                              theorem ZMod.intCast_cast_mul {n : } (x y : ZMod n) :
                              (x * y).cast = x.cast * y.cast % n
                              theorem ZMod.intCast_cast_sub {n : } (x 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
                              @[simp]
                              theorem ZMod.intCast_mod (a : ) (b : ) :
                              ↑(a % b) = a
                              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
                              theorem ZMod.val_one_eq_one_mod (n : ) :
                              val 1 = 1 % n
                              theorem ZMod.val_two_eq_two_mod (n : ) :
                              val 2 = 2 % n
                              theorem ZMod.val_one (n : ) [Fact (1 < n)] :
                              val 1 = 1
                              theorem ZMod.val_one'' {n : } :
                              n 1val 1 = 1
                              theorem ZMod.val_add {n : } [NeZero n] (a b : ZMod n) :
                              (a + b).val = (a.val + b.val) % n
                              theorem ZMod.val_add_of_lt {n : } {a 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 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 b : ZMod n} (h : n a.val + b.val) :
                              (a + b).val = a.val + b.val - n
                              theorem ZMod.val_add_le {n : } (a b : ZMod n) :
                              (a + b).val a.val + b.val
                              theorem ZMod.val_mul {n : } (a b : ZMod n) :
                              (a * b).val = a.val * b.val % n
                              theorem ZMod.val_mul_le {n : } (a b : ZMod n) :
                              (a * b).val a.val * b.val
                              theorem ZMod.val_mul_of_lt {n : } {a b : ZMod n} (h : a.val * b.val < n) :
                              (a * b).val = a.val * b.val
                              theorem ZMod.val_mul_iff_lt {n : } [NeZero n] (a b : ZMod n) :
                              (a * b).val = a.val * b.val a.val * b.val < n
                              instance ZMod.nontrivial (n : ) [Fact (1 < n)] :
                              theorem ZMod.one_eq_zero_iff {n : } :
                              1 = 0 n = 1
                              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.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
                                    theorem ZMod.eq_iff_modEq_nat (n : ) {a b : } :
                                    a = b a b [MOD n]
                                    theorem ZMod.eq_zero_iff_even {n : } :
                                    n = 0 Even n
                                    theorem ZMod.eq_one_iff_odd {n : } :
                                    n = 1 Odd n
                                    theorem ZMod.ne_zero_iff_odd {n : } :
                                    n 0 Odd 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) :
                                        (unitOfCoprime x h) = x
                                        theorem ZMod.val_coe_unit_coprime {n : } (u : (ZMod n)ˣ) :
                                        (↑u).val.Coprime 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 b : ZMod n) (h : a * b = 1) :
                                        a⁻¹ = b
                                        theorem ZMod.inv_mul_eq_one_of_isUnit {n : } {a : ZMod n} (ha : IsUnit a) (b : ZMod n) :
                                        a⁻¹ * b = 1 a = b

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

                                        Equations
                                          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
                                              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.neg_eq_self_mod_two (a : ZMod 2) :
                                                -a = a
                                                @[simp]
                                                theorem ZMod.natAbs_mod_two (a : ) :
                                                a.natAbs = a
                                                theorem ZMod.val_ne_zero {n : } (a : ZMod n) :
                                                a.val 0 a 0
                                                theorem ZMod.val_pos {n : } {a : ZMod n} :
                                                0 < a.val a 0
                                                theorem ZMod.val_eq_one {n : } :
                                                1 < n∀ (a : ZMod n), a.val = 1 a = 1
                                                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.val_cast_zmod_lt {m : } [NeZero m] (n : ) [NeZero n] (a : ZMod m) :
                                                a.cast.val < m
                                                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 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) :
                                                theorem ZMod.cast_cast_zmod_of_le {m n : } [hm : NeZero m] (h : m n) (a : ZMod m) :
                                                a.cast.cast = a
                                                theorem ZMod.val_pow {m n : } {a : ZMod n} [ilt : Fact (1 < n)] (h : a.val ^ m < n) :
                                                (a ^ m).val = a.val ^ m
                                                theorem ZMod.val_pow_le {m n : } [Fact (1 < n)] {a : ZMod n} :
                                                (a ^ m).val a.val ^ m
                                                theorem ZMod.natAbs_min_of_le_div_two (n : ) (x y : ) (he : x = y) (hl : x.natAbs n / 2) :
                                                theorem RingHom.ext_zmod {n : } {R : Type u_1} [NonAssocSemiring R] (f g : ZMod n →+* R) :
                                                f = g
                                                @[simp]
                                                theorem ZMod.ringHom_map_cast {n : } {R : Type u_1} [NonAssocRing R] (f : R →+* ZMod n) (k : ZMod n) :
                                                f k.cast = k

                                                Any ring homomorphism into ZMod n has a right inverse.

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

                                                Any ring homomorphism into ZMod n is surjective.

                                                @[simp]
                                                theorem ZMod.castHom_self {n : } :
                                                @[simp]
                                                theorem ZMod.castHom_comp {n m d : } (hm : n m) (hd : m d) :
                                                (castHom hm (ZMod n)).comp (castHom hd (ZMod m)) = 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 : ) :
                                                    ((lift n) f) x = f x
                                                    theorem ZMod.lift_castAddHom (n : ) {A : Type u_2} [AddGroup A] (f : { f : →+ A // f n = 0 }) (x : ) :
                                                    ((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 }) :
                                                    ((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 }) :
                                                    ((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 ((lift n) f) ∀ (m : ), f m = 0m = 0

                                                    Groups of bounded torsion #

                                                    For G a group and n a natural number, G having torsion dividing n (∀ x : G, n • x = 0) can be derived from Module R G where R has characteristic dividing n.

                                                    It is however painful to have the API for such groups G stated in this generality, as R does not appear anywhere in the lemmas' return type. Instead of writing the API in terms of a general R, we therefore specialise to the canonical ring of order n, namely ZMod n.

                                                    This spelling Module (ZMod n) G has the extra advantage of providing the canonical action by ZMod n. It is however Type-valued, so we might want to acquire a Prop-valued version in the future.

                                                    theorem zmod_smul_mem {n : } {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] {K : S} [Module (ZMod n) G] {x : G} (hx : x K) (a : ZMod n) :
                                                    a x K
                                                    theorem smulMemClass {n : } {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] [Module (ZMod n) G] :

                                                    This cannot be made an instance because of the [Module (ZMod n) G] argument and the fact that n only appears in the second argument of SMulMemClass, which is an OutParam.

                                                    instance AddSubgroupClass.instZModSMul {n : } {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] {K : S} [Module (ZMod n) G] :
                                                    SMul (ZMod n) K
                                                    Equations
                                                      @[simp]
                                                      theorem AddSubgroupClass.coe_zmod_smul {n : } {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] {K : S} [Module (ZMod n) G] (a : ZMod n) (x : K) :
                                                      ↑(a x) = a x
                                                      instance AddSubgroupClass.instZModModule {n : } {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] {K : S} [Module (ZMod n) G] :
                                                      Module (ZMod n) K
                                                      Equations
                                                        theorem ZModModule.char_nsmul_eq_zero (n : ) {G : Type u_2} [AddCommGroup G] [Module (ZMod n) G] (x : G) :
                                                        n x = 0
                                                        theorem ZModModule.char_ne_one (n : ) (G : Type u_2) [AddCommGroup G] [Module (ZMod n) G] [Nontrivial G] :
                                                        n 1
                                                        theorem ZModModule.two_le_char (n : ) (G : Type u_2) [AddCommGroup G] [Module (ZMod n) G] [NeZero n] [Nontrivial G] :
                                                        2 n
                                                        theorem ZModModule.periodicPts_add_left (n : ) {G : Type u_2} [AddCommGroup G] [Module (ZMod n) G] [NeZero n] (x : G) :
                                                        (Function.periodicPts fun (x_1 : G) => x + x_1) = Set.univ
                                                        theorem ZModModule.add_self {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x : G) :
                                                        x + x = 0
                                                        theorem ZModModule.neg_eq_self {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x : G) :
                                                        -x = x
                                                        theorem ZModModule.sub_eq_add {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x y : G) :
                                                        x - y = x + y
                                                        theorem ZModModule.add_add_add_cancel {G : Type u_2} [AddCommGroup G] [Module (ZMod 2) G] (x y z : G) :
                                                        x + y + (y + z) = x + z
                                                        @[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.

                                                        Equivalence between and ZMod N × ℕ, sending n to (n mod N, n / N).

                                                        Equations
                                                          Instances For