Mathlib.Data.ZMod.Basic

ZMod.finEquiv definition

: ∀ (n : ℕ) [NeZero n], Fin n ≃+* ZMod n

Full source

/-- For non-zero `n : ℕ`, the ring `Fin n` is equivalent to `ZMod n`. -/
def finEquiv : ∀ (n : ℕ) [NeZero n], FinFin n ≃+* ZMod n
  | 0, h => (h.ne _ rfl).elim
  | _ + 1, _ => .refl _

Ring isomorphism between $\text{Fin } n$ and $\mathbb{Z}/n\mathbb{Z}$ for $ n > 0 $

Informal description

For any positive integer $ n $, there is a ring isomorphism between the finite type with $ n $ elements $\text{Fin } n$ and the integers modulo $ n $ $\mathbb{Z}/n\mathbb{Z}$.

ZMod.charZero instance

: CharZero (ZMod 0)

Full source

instance charZero : CharZero (ZMod 0) := inferInstanceAs (CharZero ℤ)

Characteristic Zero of Integers Modulo Zero

Informal description

The integers modulo $0$ ($\mathbb{Z}/0\mathbb{Z} \cong \mathbb{Z}$) have characteristic zero. That is, the canonical map from the natural numbers to $\mathbb{Z}/0\mathbb{Z}$ is injective.

ZMod.val definition

: ∀ {n : ℕ}, ZMod n → ℕ

Full source

/-- `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.
-/
def val : ∀ {n : ℕ}, ZMod n → ℕ
  | 0 => Int.natAbs
  | n + 1 => ((↑) : Fin (n + 1) → ℕ)

Natural number representative of an integer modulo `n`

Informal description

The function `val` maps an element `a` of the integers modulo `n` (`ZMod n`) to a natural number defined as: - For `n = 0` (i.e., `ZMod 0` is the integers `ℤ`), `val a` is the absolute value of `a` as a natural number. - For `n > 0` (i.e., `ZMod n` is the finite type with `n` elements), `val a` is the least natural number in the equivalence class of `a`.

ZMod.val_lt theorem

{n : ℕ} [NeZero n] (a : ZMod n) : a.val < n

Full source

theorem val_lt {n : ℕ} [NeZero n] (a : ZMod n) : a.val < n := by
  cases n
  · cases NeZero.ne 0 rfl
  exact Fin.is_lt a

Natural Representative of Integer Modulo $n$ is Less Than $n$

Informal description

For any nonzero natural number $n$ and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative $\text{val}(a)$ satisfies $\text{val}(a) < n$.

ZMod.val_le theorem

{n : ℕ} [NeZero n] (a : ZMod n) : a.val ≤ n

Full source

theorem val_le {n : ℕ} [NeZero n] (a : ZMod n) : a.val ≤ n :=
  a.val_lt.le

Upper Bound on Natural Representative in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any nonzero natural number $n$ and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative $\text{val}(a)$ satisfies $\text{val}(a) \leq n$.

ZMod.val_zero theorem

: ∀ {n}, (0 : ZMod n).val = 0

Full source

@[simp]
theorem val_zero : ∀ {n}, (0 : ZMod n).val = 0
  | 0 => rfl
  | _ + 1 => rfl

Natural Representative of Zero in $\mathbb{Z}/n\mathbb{Z}$ is Zero

Informal description

For any natural number $n$, the natural number representative of the zero element in $\mathbb{Z}/n\mathbb{Z}$ is $0$, i.e., $\text{val}(0) = 0$.

ZMod.val_one' theorem

: (1 : ZMod 0).val = 1

Full source

@[simp]
theorem val_one' : (1 : ZMod 0).val = 1 :=
  rfl

Natural representative of 1 in $\mathbb{Z}/0\mathbb{Z}$ is 1

Informal description

For the integer $1$ in $\mathbb{Z}/0\mathbb{Z}$ (which is isomorphic to $\mathbb{Z}$), the natural number representative $\text{val}(1)$ is equal to $1$.

ZMod.val_neg' theorem

{n : ZMod 0} : (-n).val = n.val

Full source

@[simp]
theorem val_neg' {n : ZMod 0} : (-n).val = n.val :=
  Int.natAbs_neg n

Natural representative of negation in $\mathbb{Z}$ equals original representative

Informal description

For any integer $n$ in $\mathbb{Z}/0\mathbb{Z}$ (which is isomorphic to $\mathbb{Z}$), the natural number representative of $-n$ is equal to the natural number representative of $n$, i.e., $\text{val}(-n) = \text{val}(n)$.

ZMod.val_mul' theorem

{m n : ZMod 0} : (m * n).val = m.val * n.val

Full source

@[simp]
theorem val_mul' {m n : ZMod 0} : (m * n).val = m.val * n.val :=
  Int.natAbs_mul m n

Multiplicativity of Natural Representative in $\mathbb{Z}/0\mathbb{Z}$

Informal description

For any integers $m$ and $n$ in $\mathbb{Z}/0\mathbb{Z} \cong \mathbb{Z}$, the natural number representative of their product equals the product of their natural number representatives, i.e., $\text{val}(m \cdot n) = \text{val}(m) \cdot \text{val}(n)$.

ZMod.val_natCast theorem

(n a : ℕ) : (a : ZMod n).val = a % n

Full source

@[simp]
theorem val_natCast (n a : ℕ) : (a : ZMod n).val = a % n := by
  cases n
  · rw [Nat.mod_zero]
    exact Int.natAbs_natCast a
  · apply Fin.val_natCast

Natural Representative of Integer Modulo $n$ Equals Modulo Reduction

Informal description

For any natural numbers $n$ and $a$, the natural number representative of the cast of $a$ into $\mathbb{Z}/n\mathbb{Z}$ is equal to $a$ modulo $n$, i.e., $\text{val}(a \bmod n) = a \bmod n$.

ZMod.val_natCast_of_lt theorem

{n a : ℕ} (h : a < n) : (a : ZMod n).val = a

Full source

lemma val_natCast_of_lt {n a : ℕ} (h : a < n) : (a : ZMod n).val = a := by
  rwa [val_natCast, Nat.mod_eq_of_lt]

Natural Representative of Small Integer Modulo $n$ Equals Itself

Informal description

For any natural numbers $n$ and $a$ such that $a < n$, the natural number representative of the image of $a$ in $\mathbb{Z}/n\mathbb{Z}$ is equal to $a$ itself, i.e., $\text{val}(a \bmod n) = a$.

ZMod.val_ofNat theorem

(n a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ZMod n).val = ofNat(a) % n

Full source

lemma val_ofNat (n a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ZMod n).val = ofNat(a) % n := val_natCast ..

Natural Representative of Canonical Embedding in $\mathbb{Z}/n\mathbb{Z}$ Equals Modulo Reduction for $a \geq 2$

Informal description

For any natural numbers $n$ and $a \geq 2$, the natural number representative of the canonical embedding of $a$ into $\mathbb{Z}/n\mathbb{Z}$ is equal to $a \bmod n$, i.e., $\text{val}(a \bmod n) = a \bmod n$.

ZMod.val_ofNat_of_lt theorem

{n a : ℕ} [a.AtLeastTwo] (han : a < n) : (ofNat(a) : ZMod n).val = ofNat(a)

Full source

lemma val_ofNat_of_lt {n a : ℕ} [a.AtLeastTwo] (han : a < n) : (ofNat(a) : ZMod n).val = ofNat(a) :=
  val_natCast_of_lt han

Natural Representative of Canonical Embedding in $\mathbb{Z}/n\mathbb{Z}$ Equals Itself for $a \geq 2$ and $a < n$

Informal description

For any natural numbers $n$ and $a \geq 2$ such that $a < n$, the natural number representative of the canonical embedding of $a$ into $\mathbb{Z}/n\mathbb{Z}$ is equal to $a$ itself, i.e., $\text{val}(a \bmod n) = a$.

ZMod.val_unit' theorem

{n : ZMod 0} : IsUnit n ↔ n.val = 1

Full source

theorem val_unit' {n : ZMod 0} : IsUnitIsUnit n ↔ n.val = 1 := by
  simp only [val]
  rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]

Characterization of Units in Integers: $|n| = 1$

Informal description

For an integer `n` in `ℤ` (represented as `ZMod 0`), `n` is a unit if and only if its absolute value as a natural number is equal to 1, i.e., `|n| = 1`.

ZMod.charP instance

(n : ℕ) : CharP (ZMod n) n

Full source

instance charP (n : ℕ) : CharP (ZMod n) n where
  cast_eq_zero_iff := by
    intro k
    rcases n with - | n
    · simp [zero_dvd_iff, Int.natCast_eq_zero]
    · exact Fin.natCast_eq_zero

Characteristic of Integers Modulo $n$ is $n$

Informal description

For any natural number $n$, the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) have characteristic $n$. That is, the smallest positive integer $p$ such that $p \cdot 1 = 0$ in $\mathbb{Z}/n\mathbb{Z}$ is $n$ itself.

ZMod.addOrderOf_one theorem

(n : ℕ) : addOrderOf (1 : ZMod n) = n

Full source

@[simp]
theorem addOrderOf_one (n : ℕ) : addOrderOf (1 : ZMod n) = n :=
  CharP.eq _ (CharP.addOrderOf_one _) (ZMod.charP n)

Additive Order of Unity in $\mathbb{Z}/n\mathbb{Z}$ is $n$

Informal description

For any natural number $n$, the additive order of the multiplicative identity $1$ in the ring of integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) is equal to $n$. That is, the smallest positive integer $k$ such that $k \cdot 1 = 0$ in $\mathbb{Z}/n\mathbb{Z}$ is $n$ itself.

ZMod.addOrderOf_coe theorem

(a : ℕ) {n : ℕ} (n0 : n ≠ 0) : addOrderOf (a : ZMod n) = n / n.gcd a

Full source

/-- 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 addOrderOf_coe (a : ℕ) {n : ℕ} (n0 : n ≠ 0) : addOrderOf (a : ZMod n) = n / n.gcd a := by
  rcases a with - | a
  · simp only [Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right,
      Nat.pos_of_ne_zero n0, Nat.div_self]
  rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]

Additive Order Formula in $\mathbb{Z}/n\mathbb{Z}$: $\text{addOrderOf}(a) = n / \gcd(n, a)$ for $n \neq 0$

Informal description

For any natural numbers $a$ and $n$ with $n \neq 0$, the additive order of $a$ in $\mathbb{Z}/n\mathbb{Z}$ is equal to $n$ divided by the greatest common divisor of $n$ and $a$, i.e., $\text{addOrderOf}(a) = n / \gcd(n, a)$.

ZMod.addOrderOf_coe' theorem

{a : ℕ} (n : ℕ) (a0 : a ≠ 0) : addOrderOf (a : ZMod n) = n / n.gcd a

Full source

/-- 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`. -/
@[simp]
theorem addOrderOf_coe' {a : ℕ} (n : ℕ) (a0 : a ≠ 0) : addOrderOf (a : ZMod n) = n / n.gcd a := by
  rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]

Additive Order of Nonzero Element in $\mathbb{Z}/n\mathbb{Z}$ is $n/\gcd(n,a)$

Informal description

For any nonzero natural number $a$ and any natural number $n$, the additive order of the element $a$ in the ring $\mathbb{Z}/n\mathbb{Z}$ is given by $\frac{n}{\gcd(n, a)}$.

ZMod.ringChar_zmod_n theorem

(n : ℕ) : ringChar (ZMod n) = n

Full source

/-- We have that `ringChar (ZMod n) = n`. -/
theorem ringChar_zmod_n (n : ℕ) : ringChar (ZMod n) = n := by
  rw [ringChar.eq_iff]
  exact ZMod.charP n

Ring Characteristic of $\mathbb{Z}/n\mathbb{Z}$ is $n$

Informal description

For any natural number $n$, the ring characteristic of the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) is equal to $n$, i.e., $\text{ringChar}(\mathbb{Z}/n\mathbb{Z}) = n$.

ZMod.natCast_self theorem

(n : ℕ) : (n : ZMod n) = 0

Full source

theorem natCast_self (n : ℕ) : (n : ZMod n) = 0 :=
  CharP.cast_eq_zero (ZMod n) n

$n \equiv 0 \pmod{n}$ (self-congruence in $\mathbb{Z}/n\mathbb{Z}$)

Informal description

For any natural number $n$, the canonical image of $n$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) is equal to zero, i.e., $n \equiv 0 \pmod{n}$.

ZMod.natCast_self' theorem

(n : ℕ) : (n + 1 : ZMod (n + 1)) = 0

Full source

@[simp]
theorem natCast_self' (n : ℕ) : (n + 1 : ZMod (n + 1)) = 0 := by
  rw [← Nat.cast_add_one, natCast_self (n + 1)]

$n + 1 \equiv 0 \pmod{n + 1}$ (self-congruence in $\mathbb{Z}/(n+1)\mathbb{Z}$)

Informal description

For any natural number $n$, the canonical image of $n + 1$ in the integers modulo $n + 1$ ($\mathbb{Z}/(n+1)\mathbb{Z}$) is equal to zero, i.e., $n + 1 \equiv 0 \pmod{n + 1}$.

ZMod.cast definition

: ∀ {n : ℕ}, ZMod n → R

Full source

/-- 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. -/
def cast : ∀ {n : ℕ}, ZMod n → R
  | 0 => Int.cast
  | _ + 1 => fun i => i.val

Canonical map from integers modulo $ n $ to a semiring

Informal description

The function maps an element of the integers modulo $ n $ ($ \mathbb{Z}/n\mathbb{Z} $) to an element of a semiring $ R $. Specifically: - When $ n = 0 $, it uses the canonical integer coercion $ \mathbb{Z} \to R $. - When $ n > 0 $, it maps the element to its least natural number representative in $ R $. This function is a ring homomorphism if the characteristic of $ R $ divides $ n $.

ZMod.cast_zero theorem

: (cast (0 : ZMod n) : R) = 0

Full source

@[simp]
theorem cast_zero : (cast (0 : ZMod n) : R) = 0 := by
  delta ZMod.cast
  cases n
  · exact Int.cast_zero
  · simp

Canonical Map Preserves Zero: $\operatorname{cast}(0) = 0$ in $\mathbb{Z}/n\mathbb{Z} \to R$

Informal description

For any natural number $n$ and any semiring $R$, the canonical map from $\mathbb{Z}/n\mathbb{Z}$ to $R$ maps the zero element of $\mathbb{Z}/n\mathbb{Z}$ to the zero element of $R$, i.e., $\operatorname{cast}(0) = 0$.

ZMod.cast_eq_val theorem

[NeZero n] (a : ZMod n) : (cast a : R) = a.val

Full source

theorem cast_eq_val [NeZero n] (a : ZMod n) : (cast a : R) = a.val := by
  cases n
  · cases NeZero.ne 0 rfl
  rfl

Canonical map equals least representative in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any nonzero natural number $ n $ and any element $ a $ in the integers modulo $ n $ ($ \mathbb{Z}/n\mathbb{Z} $), the canonical map $ \operatorname{cast} $ from $ \mathbb{Z}/n\mathbb{Z} $ to a semiring $ R $ satisfies $ \operatorname{cast}(a) = \operatorname{val}(a) $, where $ \operatorname{val}(a) $ is the least natural number representative of $ a $ in $ \mathbb{Z}/n\mathbb{Z} $.

Prod.fst_zmod_cast theorem

(a : ZMod n) : (cast a : R × S).fst = cast a

Full source

@[simp]
theorem _root_.Prod.fst_zmod_cast (a : ZMod n) : (cast a : R × S).fst = cast a := by
  cases n
  · rfl
  · simp [ZMod.cast]

First Projection of Canonical Map from $\mathbb{Z}/n\mathbb{Z}$ to $R \times S$ Equals Canonical Map to $R$

Informal description

For any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the first projection of the canonical map $\operatorname{cast}(a)$ in the product semiring $R \times S$ equals the canonical map $\operatorname{cast}(a)$ in $R$. That is, $\pi_1(\operatorname{cast}(a)) = \operatorname{cast}(a) \in R$.

Prod.snd_zmod_cast theorem

(a : ZMod n) : (cast a : R × S).snd = cast a

Full source

@[simp]
theorem _root_.Prod.snd_zmod_cast (a : ZMod n) : (cast a : R × S).snd = cast a := by
  cases n
  · rfl
  · simp [ZMod.cast]

Second Projection of Canonical Map in Product Ring Equals Canonical Map in Second Component

Informal description

For any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the second projection of the canonical map $\operatorname{cast}(a)$ in the product ring $R \times S$ equals the canonical map $\operatorname{cast}(a)$ in $S$. That is, $\pi_2(\operatorname{cast}(a)) = \operatorname{cast}(a) \in S$.

ZMod.natCast_zmod_val theorem

{n : ℕ} [NeZero n] (a : ZMod n) : (a.val : ZMod n) = a

Full source

/-- So-named because the coercion is `Nat.cast` into `ZMod`. For `Nat.cast` into an arbitrary ring,
see `ZMod.natCast_val`. -/
theorem natCast_zmod_val {n : ℕ} [NeZero n] (a : ZMod n) : (a.val : ZMod n) = a := by
  cases n
  · cases NeZero.ne 0 rfl
  · apply Fin.cast_val_eq_self

Natural Representative Casting Identity in $\mathbb{Z}/n\mathbb{Z}$: $ (a.\mathrm{val} : \mathbb{Z}/n\mathbb{Z}) = a $

Informal description

For any positive integer $ n $ and any element $ a $ in the integers modulo $ n $ ($\mathbb{Z}/n\mathbb{Z}$), casting the natural number representative $ a.\mathrm{val} $ back to $\mathbb{Z}/n\mathbb{Z}$ yields $ a $ itself, i.e., $ (a.\mathrm{val} : \mathbb{Z}/n\mathbb{Z}) = a $.

ZMod.natCast_rightInverse theorem

[NeZero n] : Function.RightInverse val ((↑) : ℕ → ZMod n)

Full source

theorem natCast_rightInverse [NeZero n] : Function.RightInverse val ((↑) : ℕ → ZMod n) :=
  natCast_zmod_val

Right Inverse Property of Natural Number Representative in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any positive integer $ n $, the function $\mathrm{val} : \mathbb{Z}/n\mathbb{Z} \to \mathbb{N}$ is a right inverse of the canonical map $(\cdot) : \mathbb{N} \to \mathbb{Z}/n\mathbb{Z}$. That is, for any natural number $ k $, we have $\mathrm{val}(k \bmod n) = k \bmod n$.

ZMod.natCast_zmod_surjective theorem

[NeZero n] : Function.Surjective ((↑) : ℕ → ZMod n)

Full source

theorem natCast_zmod_surjective [NeZero n] : Function.Surjective ((↑) : ℕ → ZMod n) :=
  natCast_rightInverse.surjective

Surjectivity of Natural Number Casting to $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any positive integer $n$, the canonical map from the natural numbers $\mathbb{N}$ to the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) is surjective. That is, every element of $\mathbb{Z}/n\mathbb{Z}$ can be represented as the image of some natural number under this map.

ZMod.intCast_zmod_cast theorem

(a : ZMod n) : ((cast a : ℤ) : ZMod n) = a

Full source

/-- So-named because the outer coercion is `Int.cast` into `ZMod`. For `Int.cast` into an arbitrary
ring, see `ZMod.intCast_cast`. -/
@[norm_cast]
theorem intCast_zmod_cast (a : ZMod n) : ((cast a : ℤ) : ZMod n) = a := by
  cases n
  · simp [ZMod.cast, ZMod]
  · dsimp [ZMod.cast]
    rw [Int.cast_natCast, natCast_zmod_val]

Identity for Integer Casting in $\mathbb{Z}/n\mathbb{Z}$: $(\text{cast}(a) : \mathbb{Z}) \text{ mod } n = a$

Informal description

For any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the composition of the canonical map from $\mathbb{Z}/n\mathbb{Z}$ to $\mathbb{Z}$ followed by the canonical map from $\mathbb{Z}$ back to $\mathbb{Z}/n\mathbb{Z}$ returns $a$ itself. In other words, if we first cast $a$ to an integer and then cast that integer back to $\mathbb{Z}/n\mathbb{Z}$, we recover $a$.

ZMod.intCast_rightInverse theorem

: Function.RightInverse (cast : ZMod n → ℤ) ((↑) : ℤ → ZMod n)

Full source

theorem intCast_rightInverse : Function.RightInverse (cast : ZMod n → ℤ) ((↑) : ℤ → ZMod n) :=
  intCast_zmod_cast

Right Inverse Property of Integer Casting in $\mathbb{Z}/n\mathbb{Z}$: $\text{cast}(x \bmod n) = x \bmod n$

Informal description

The canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}$ is a right inverse of the canonical map $\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$. That is, for any integer $x \in \mathbb{Z}$, we have $\text{cast}(x \bmod n) = x$ when interpreted modulo $n$.

ZMod.intCast_surjective theorem

: Function.Surjective ((↑) : ℤ → ZMod n)

Full source

theorem intCast_surjective : Function.Surjective ((↑) : ℤ → ZMod n) :=
  intCast_rightInverse.surjective

Surjectivity of the Canonical Map $\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$

Informal description

The canonical map from the integers $\mathbb{Z}$ to the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) is surjective. That is, for every element $a \in \mathbb{Z}/n\mathbb{Z}$, there exists an integer $x \in \mathbb{Z}$ such that $x \bmod n = a$.

ZMod.forall theorem

{P : ZMod n → Prop} : (∀ x, P x) ↔ ∀ x : ℤ, P x

Full source

lemma «forall» {P : ZMod n → Prop} : (∀ x, P x) ↔ ∀ x : ℤ, P x := intCast_surjective.forall

Universal Quantifier Transfer for Integers Modulo $n$

Informal description

For any predicate $P$ on the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the statement $(\forall x \in \mathbb{Z}/n\mathbb{Z}, P(x))$ holds if and only if $(\forall x \in \mathbb{Z}, P(x \bmod n))$ holds.

ZMod.exists theorem

{P : ZMod n → Prop} : (∃ x, P x) ↔ ∃ x : ℤ, P x

Full source

lemma «exists» {P : ZMod n → Prop} : (∃ x, P x) ↔ ∃ x : ℤ, P x := intCast_surjective.exists

Existence Transfer between $\mathbb{Z}$ and $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any predicate $P$ on the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), there exists an element $x \in \mathbb{Z}/n\mathbb{Z}$ satisfying $P(x)$ if and only if there exists an integer $k \in \mathbb{Z}$ such that $P(k \bmod n)$ holds.

ZMod.cast_id theorem

: ∀ (n) (i : ZMod n), (ZMod.cast i : ZMod n) = i

Full source

theorem cast_id : ∀ (n) (i : ZMod n), (ZMod.cast i : ZMod n) = i
  | 0, _ => Int.cast_id
  | _ + 1, i => natCast_zmod_val i

Identity Property of the Canonical Map in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $ n $ and any element $ i $ in the integers modulo $ n $ ($\mathbb{Z}/n\mathbb{Z}$), the canonical map $\mathrm{cast}$ from $\mathbb{Z}/n\mathbb{Z}$ to itself satisfies $\mathrm{cast}(i) = i$.

ZMod.cast_id' theorem

: (ZMod.cast : ZMod n → ZMod n) = id

Full source

@[simp]
theorem cast_id' : (ZMod.cast : ZMod n → ZMod n) = id :=
  funext (cast_id n)

Identity of the Canonical Map on $\mathbb{Z}/n\mathbb{Z}$: $\mathrm{cast} = \mathrm{id}$

Informal description

The canonical map $\mathrm{cast} \colon \mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ is equal to the identity function, i.e., $\mathrm{cast} = \mathrm{id}$.

ZMod.natCast_comp_val theorem

[NeZero n] : ((↑) : ℕ → R) ∘ (val : ZMod n → ℕ) = cast

Full source

/-- The coercions are respectively `Nat.cast` and `ZMod.cast`. -/
@[simp]
theorem natCast_comp_val [NeZero n] : ((↑) : ℕ → R) ∘ (val : ZMod n → ℕ) = cast := by
  cases n
  · cases NeZero.ne 0 rfl
  rfl

Compatibility of Natural Number Representative and Canonical Map in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any nonzero natural number $ n $ (i.e., `NeZero n` holds), the composition of the canonical map from natural numbers to a semiring $ R $ with the natural number representative function `val` on $\mathbb{Z}/n\mathbb{Z}$ is equal to the canonical map `cast` from $\mathbb{Z}/n\mathbb{Z}$ to $ R $. In other words, for any $ i \in \mathbb{Z}/n\mathbb{Z} $, we have $ \text{val}(i) $ as a natural number, and its image under the canonical map $ \mathbb{N} \to R $ is equal to the image of $ i $ under the canonical map $ \mathbb{Z}/n\mathbb{Z} \to R $.

ZMod.intCast_comp_cast theorem

: ((↑) : ℤ → R) ∘ (cast : ZMod n → ℤ) = cast

Full source

/-- The coercions are respectively `Int.cast`, `ZMod.cast`, and `ZMod.cast`. -/
@[simp]
theorem intCast_comp_cast : ((↑) : ℤ → R) ∘ (cast : ZMod n → ℤ) = cast := by
  cases n
  · exact congr_arg (Int.castInt.cast ∘ ·) ZMod.cast_id'
  · ext
    simp [ZMod, ZMod.cast]

Compatibility of Integer Coercion and Canonical Map from $\mathbb{Z}/n\mathbb{Z}$ to $R$

Informal description

For any ring $R$, the composition of the canonical integer coercion $\mathbb{Z} \to R$ with the canonical map $\mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}$ equals the canonical map $\mathbb{Z}/n\mathbb{Z} \to R$. In other words, the following diagram commutes: \[ \mathbb{Z}/n\mathbb{Z} \xrightarrow{\text{cast}} \mathbb{Z} \xrightarrow{\text{canonical}} R = \mathbb{Z}/n\mathbb{Z} \xrightarrow{\text{cast}} R \]

ZMod.natCast_val theorem

[NeZero n] (i : ZMod n) : (i.val : R) = cast i

Full source

@[simp]
theorem natCast_val [NeZero n] (i : ZMod n) : (i.val : R) = cast i :=
  congr_fun (natCast_comp_val R) i

Natural Number Representative Equals Canonical Image in $ \mathbb{Z}/n\mathbb{Z} $

Informal description

For any nonzero natural number $ n $ (i.e., $ n \neq 0 $) and any element $ i $ of the integers modulo $ n $ ($ \mathbb{Z}/n\mathbb{Z} $), the image of the natural number representative $ \text{val}(i) $ under the canonical map $ \mathbb{N} \to R $ is equal to the image of $ i $ under the canonical map $ \mathbb{Z}/n\mathbb{Z} \to R $. In other words, $ \text{val}(i) $ as an element of $ R $ equals the canonical image of $ i $ in $ R $.

ZMod.intCast_cast theorem

(i : ZMod n) : ((cast i : ℤ) : R) = cast i

Full source

@[simp]
theorem intCast_cast (i : ZMod n) : ((cast i : ℤ) : R) = cast i :=
  congr_fun (intCast_comp_cast R) i

Compatibility of Integer Casting in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any element $i$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the integer obtained by first casting $i$ to $\mathbb{Z}$ and then to a ring $R$ is equal to directly casting $i$ to $R$. In other words, the following diagram commutes: \[ \mathbb{Z}/n\mathbb{Z} \xrightarrow{\text{cast}} \mathbb{Z} \xrightarrow{\text{canonical}} R = \mathbb{Z}/n\mathbb{Z} \xrightarrow{\text{cast}} R \]

ZMod.cast_add_eq_ite theorem

 {n : ℕ} (a b : ZMod n) :
  (cast (a + b) : ℤ) = if (n : ℤ) ≤ cast a + cast b then (cast a + cast b - n : ℤ) else cast a + cast b

Full source

theorem cast_add_eq_ite {n : ℕ} (a b : ZMod n) :
    (cast (a + b) : ℤ) =
      if (n : ℤ) ≤ cast a + cast b then (cast a + cast b - n : ℤ) else cast a + cast b := by
  rcases n with - | n
  · simp; rfl
  change Fin (n + 1) at a b
  change ((((a + b) : Fin (n + 1)) : ℕ) : ℤ) = if ((n + 1 : ℕ) : ℤ) ≤ (a : ℕ) + b then _ else _
  simp only [Fin.val_add_eq_ite, Int.natCast_succ, Int.ofNat_le]
  norm_cast
  split_ifs with h
  · rw [Nat.cast_sub h]
    congr
  · rfl

Integer Representation of Sum in $\mathbb{Z}/n\mathbb{Z}$ with Modular Condition

Informal description

For any natural number $n$ and elements $a, b$ of the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the integer value of their sum under the canonical map is given by: \[ \text{cast}(a + b) = \begin{cases} \text{cast}(a) + \text{cast}(b) - n & \text{if } n \leq \text{cast}(a) + \text{cast}(b), \\ \text{cast}(a) + \text{cast}(b) & \text{otherwise.} \end{cases} \] Here, $\text{cast}(x)$ denotes the canonical integer representation of $x \in \mathbb{Z}/n\mathbb{Z}$.

ZMod.cast_one theorem

(h : m ∣ n) : (cast (1 : ZMod n) : R) = 1

Full source

@[simp]
theorem cast_one (h : m ∣ n) : (cast (1 : ZMod n) : R) = 1 := by
  rcases n with - | n
  · exact Int.cast_one
  show ((1 % (n + 1) : ℕ) : R) = 1
  cases n
  · rw [Nat.dvd_one] at h
    subst m
    subsingleton [CharP.CharOne.subsingleton]
  rw [Nat.mod_eq_of_lt]
  · exact Nat.cast_one
  exact Nat.lt_of_sub_eq_succ rfl

Canonical map preserves multiplicative identity in $\mathbb{Z}/n\mathbb{Z}$ when $m \mid n$

Informal description

For any natural numbers $m$ and $n$ such that $m$ divides $n$, the canonical map from $\mathbb{Z}/n\mathbb{Z}$ to a ring $R$ maps the multiplicative identity $1$ in $\mathbb{Z}/n\mathbb{Z}$ to the multiplicative identity $1$ in $R$.

ZMod.cast_add theorem

(h : m ∣ n) (a b : ZMod n) : (cast (a + b : ZMod n) : R) = cast a + cast b

Full source

theorem cast_add (h : m ∣ n) (a b : ZMod n) : (cast (a + b : ZMod n) : R) = cast a + cast b := by
  cases n
  · apply Int.cast_add
  symm
  dsimp [ZMod, ZMod.cast, ZMod.val]
  rw [← Nat.cast_add, Fin.val_add, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]
  exact h.trans (Nat.dvd_sub_mod _)

Canonical map preserves addition in $\mathbb{Z}/n\mathbb{Z}$ when characteristic divides $n$

Informal description

Let $m$ and $n$ be natural numbers such that $m$ divides $n$. For any elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ preserves addition, i.e., $\text{cast}(a + b) = \text{cast}(a) + \text{cast}(b)$ in the ring $R$.

ZMod.cast_mul theorem

(h : m ∣ n) (a b : ZMod n) : (cast (a * b : ZMod n) : R) = cast a * cast b

Full source

theorem cast_mul (h : m ∣ n) (a b : ZMod n) : (cast (a * b : ZMod n) : R) = cast a * cast b := by
  cases n
  · apply Int.cast_mul
  symm
  dsimp [ZMod, ZMod.cast, ZMod.val]
  rw [← Nat.cast_mul, Fin.val_mul, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]
  exact h.trans (Nat.dvd_sub_mod _)

Canonical map preserves multiplication in $\mathbb{Z}/n\mathbb{Z}$ when characteristic divides $n$

Informal description

Let $m$ and $n$ be natural numbers such that $m$ divides $n$. For any elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ satisfies $\text{cast}(a \cdot b) = \text{cast}(a) \cdot \text{cast}(b)$ in the ring $R$.

ZMod.castHom definition

(h : m ∣ n) (R : Type*) [Ring R] [CharP R m] : ZMod n →+* R

Full source

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

See also `ZMod.lift` for a generalized version working in `AddGroup`s.
-/
def castHom (h : m ∣ n) (R : Type*) [Ring R] [CharP R m] : ZModZMod n →+* R where
  toFun := cast
  map_zero' := cast_zero
  map_one' := cast_one h
  map_add' := cast_add h
  map_mul' := cast_mul h

Canonical ring homomorphism from $\mathbb{Z}/n\mathbb{Z}$ to a ring of characteristic dividing $n$

Informal description

Given natural numbers $ m $ and $ n $ such that $ m $ divides $ n $, and a ring $ R $ of characteristic $ m $, the function `ZMod.castHom` is the canonical ring homomorphism from the integers modulo $ n $ ($ \mathbb{Z}/n\mathbb{Z} $) to $ R $. It maps an element $ a $ of $ \mathbb{Z}/n\mathbb{Z} $ to its image in $ R $ via the canonical map `cast`, and satisfies the properties of a ring homomorphism: - $ \text{castHom}(0) = 0 $ - $ \text{castHom}(1) = 1 $ - $ \text{castHom}(a + b) = \text{castHom}(a) + \text{castHom}(b) $ - $ \text{castHom}(a \cdot b) = \text{castHom}(a) \cdot \text{castHom}(b) $

ZMod.castHom_apply theorem

{h : m ∣ n} (i : ZMod n) : castHom h R i = cast i

Full source

@[simp]
theorem castHom_apply {h : m ∣ n} (i : ZMod n) : castHom h R i = cast i :=
  rfl

Canonical Ring Homomorphism from $\mathbb{Z}/n\mathbb{Z}$ to $R$ Coincides with Cast Function

Informal description

For any natural numbers $ m $ and $ n $ such that $ m $ divides $ n $, and any ring $ R $ of characteristic $ m $, the canonical ring homomorphism $\text{castHom} : \mathbb{Z}/n\mathbb{Z} \to R$ satisfies $\text{castHom}(i) = \text{cast}(i)$ for every element $ i \in \mathbb{Z}/n\mathbb{Z} $.

ZMod.cast_sub theorem

(h : m ∣ n) (a b : ZMod n) : (cast (a - b : ZMod n) : R) = cast a - cast b

Full source

@[simp]
theorem cast_sub (h : m ∣ n) (a b : ZMod n) : (cast (a - b : ZMod n) : R) = cast a - cast b :=
  (castHom h R).map_sub a b

Subtraction Preservation Under Canonical Map from $\mathbb{Z}/n\mathbb{Z}$ to Ring of Characteristic Dividing $n$

Informal description

Let $m$ and $n$ be natural numbers such that $m$ divides $n$, and let $R$ be a ring of characteristic $m$. For any elements $a, b \in \mathbb{Z}/n\mathbb{Z}$, the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ satisfies $\text{cast}(a - b) = \text{cast}(a) - \text{cast}(b)$.

ZMod.cast_neg theorem

(h : m ∣ n) (a : ZMod n) : (cast (-a : ZMod n) : R) = -(cast a)

Full source

@[simp]
theorem cast_neg (h : m ∣ n) (a : ZMod n) : (cast (-a : ZMod n) : R) = -(cast a) :=
  (castHom h R).map_neg a

Negation Preservation under Canonical Map from $\mathbb{Z}/n\mathbb{Z}$ to Ring $R$

Informal description

Let $m$ and $n$ be natural numbers such that $m$ divides $n$, and let $R$ be a ring of characteristic $m$. For any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the canonical map $\text{cast}$ satisfies $\text{cast}(-a) = -\text{cast}(a)$ in $R$.

ZMod.cast_pow theorem

(h : m ∣ n) (a : ZMod n) (k : ℕ) : (cast (a ^ k : ZMod n) : R) = (cast a) ^ k

Full source

@[simp]
theorem cast_pow (h : m ∣ n) (a : ZMod n) (k : ℕ) : (cast (a ^ k : ZMod n) : R) = (cast a) ^ k :=
  (castHom h R).map_pow a k

Power Preservation under Canonical Map from $\mathbb{Z}/n\mathbb{Z}$ to Ring of Characteristic Dividing $n$

Informal description

Let $m$ and $n$ be natural numbers such that $m$ divides $n$, and let $R$ be a ring of characteristic $m$. For any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) and any natural number $k$, the canonical map $\text{cast}$ satisfies $\text{cast}(a^k) = (\text{cast } a)^k$ in $R$.

ZMod.cast_natCast theorem

(h : m ∣ n) (k : ℕ) : (cast (k : ZMod n) : R) = k

Full source

@[simp, norm_cast]
theorem cast_natCast (h : m ∣ n) (k : ℕ) : (cast (k : ZMod n) : R) = k :=
  map_natCast (castHom h R) k

Preservation of natural numbers under canonical map from $\mathbb{Z}/n\mathbb{Z}$ to $R$

Informal description

Let $m$ and $n$ be natural numbers such that $m$ divides $n$, and let $R$ be a ring of characteristic $m$. For any natural number $k$, the canonical map from $\mathbb{Z}/n\mathbb{Z}$ to $R$ sends the image of $k$ in $\mathbb{Z}/n\mathbb{Z}$ to $k$ itself in $R$.

ZMod.cast_intCast theorem

(h : m ∣ n) (k : ℤ) : (cast (k : ZMod n) : R) = k

Full source

@[simp, norm_cast]
theorem cast_intCast (h : m ∣ n) (k : ℤ) : (cast (k : ZMod n) : R) = k :=
  map_intCast (castHom h R) k

Preservation of integer scalars under canonical map from $\mathbb{Z}/n\mathbb{Z}$ to $R$

Informal description

Let $m$ and $n$ be natural numbers such that $m$ divides $n$, and let $R$ be a ring of characteristic $m$. For any integer $k \in \mathbb{Z}$, the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ satisfies $\text{cast}(k) = k$, where $k$ on the left is interpreted as an element of $\mathbb{Z}/n\mathbb{Z}$ and $k$ on the right is interpreted as an element of $R$.

ZMod.cast_one' theorem

: (cast (1 : ZMod n) : R) = 1

Full source

@[simp]
theorem cast_one' : (cast (1 : ZMod n) : R) = 1 :=
  cast_one dvd_rfl

Preservation of multiplicative identity under canonical map from $\mathbb{Z}/n\mathbb{Z}$ to $R$

Informal description

The canonical map from the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) to a ring $R$ maps the multiplicative identity $1$ in $\mathbb{Z}/n\mathbb{Z}$ to the multiplicative identity $1$ in $R$.

ZMod.cast_add' theorem

(a b : ZMod n) : (cast (a + b : ZMod n) : R) = cast a + cast b

Full source

@[simp]
theorem cast_add' (a b : ZMod n) : (cast (a + b : ZMod n) : R) = cast a + cast b :=
  cast_add dvd_rfl a b

Canonical Map Preserves Addition in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ preserves addition, i.e., $\text{cast}(a + b) = \text{cast}(a) + \text{cast}(b)$ in the ring $R$.

ZMod.cast_mul' theorem

(a b : ZMod n) : (cast (a * b : ZMod n) : R) = cast a * cast b

Full source

@[simp]
theorem cast_mul' (a b : ZMod n) : (cast (a * b : ZMod n) : R) = cast a * cast b :=
  cast_mul dvd_rfl a b

Canonical map preserves multiplication in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ preserves multiplication, i.e., $\text{cast}(a \cdot b) = \text{cast}(a) \cdot \text{cast}(b)$ in the ring $R$.

ZMod.cast_sub' theorem

(a b : ZMod n) : (cast (a - b : ZMod n) : R) = cast a - cast b

Full source

@[simp]
theorem cast_sub' (a b : ZMod n) : (cast (a - b : ZMod n) : R) = cast a - cast b :=
  cast_sub dvd_rfl a b

Subtraction Preservation Under Canonical Map from $\mathbb{Z}/n\mathbb{Z}$ to Ring $R$

Informal description

For any elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ preserves subtraction, i.e., $\text{cast}(a - b) = \text{cast}(a) - \text{cast}(b)$ in the ring $R$.

ZMod.cast_pow' theorem

(a : ZMod n) (k : ℕ) : (cast (a ^ k : ZMod n) : R) = (cast a : R) ^ k

Full source

@[simp]
theorem cast_pow' (a : ZMod n) (k : ℕ) : (cast (a ^ k : ZMod n) : R) = (cast a : R) ^ k :=
  cast_pow dvd_rfl a k

Power Preservation under Canonical Map from $\mathbb{Z}/n\mathbb{Z}$ to Ring $R$

Informal description

For any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) and any natural number $k$, the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ preserves powers, i.e., $\text{cast}(a^k) = (\text{cast } a)^k$ in the ring $R$.

ZMod.cast_natCast' theorem

(k : ℕ) : (cast (k : ZMod n) : R) = k

Full source

@[simp, norm_cast]
theorem cast_natCast' (k : ℕ) : (cast (k : ZMod n) : R) = k :=
  cast_natCast dvd_rfl k

Preservation of Natural Numbers under Canonical Map from $\mathbb{Z}/n\mathbb{Z}$ to $R$

Informal description

For any natural number $k$, the canonical map from $\mathbb{Z}/n\mathbb{Z}$ to a semiring $R$ sends the image of $k$ in $\mathbb{Z}/n\mathbb{Z}$ to $k$ itself in $R$.

ZMod.cast_intCast' theorem

(k : ℤ) : (cast (k : ZMod n) : R) = k

Full source

@[simp, norm_cast]
theorem cast_intCast' (k : ℤ) : (cast (k : ZMod n) : R) = k :=
  cast_intCast dvd_rfl k

Preservation of integer scalars under canonical map from $\mathbb{Z}/n\mathbb{Z}$ to $R$

Informal description

For any integer $k \in \mathbb{Z}$, the canonical map $\text{cast} : \mathbb{Z}/n\mathbb{Z} \to R$ satisfies $\text{cast}(k) = k$, where $k$ on the left is interpreted as an element of $\mathbb{Z}/n\mathbb{Z}$ and $k$ on the right is interpreted as an element of $R$.

ZMod.castHom_injective theorem

: Function.Injective (ZMod.castHom (dvd_refl n) R)

Full source

theorem castHom_injective : Function.Injective (ZMod.castHom (dvd_refl n) R) := by
  rw [injective_iff_map_eq_zero]
  intro x
  obtain ⟨k, rfl⟩ := ZMod.intCast_surjective x
  rw [map_intCast, CharP.intCast_eq_zero_iff R n, CharP.intCast_eq_zero_iff (ZMod n) n]
  exact id

Injectivity of the Canonical Homomorphism from $\mathbb{Z}/n\mathbb{Z}$ to a Ring of Characteristic Dividing $n$

Informal description

The canonical ring homomorphism $\text{castHom} : \mathbb{Z}/n\mathbb{Z} \to R$ is injective, where $R$ is a ring of characteristic dividing $n$. That is, for any $a, b \in \mathbb{Z}/n\mathbb{Z}$, if $\text{castHom}(a) = \text{castHom}(b)$, then $a = b$.

ZMod.castHom_bijective theorem

[Fintype R] (h : Fintype.card R = n) : Function.Bijective (ZMod.castHom (dvd_refl n) R)

Full source

theorem castHom_bijective [Fintype R] (h : Fintype.card R = n) :
    Function.Bijective (ZMod.castHom (dvd_refl n) R) := by
  haveI : NeZero n :=
    ⟨by
      intro hn
      rw [hn] at h
      exact (Fintype.card_eq_zero_iff.mp h).elim' 0⟩
  rw [Fintype.bijective_iff_injective_and_card, ZMod.card, h, eq_self_iff_true, and_true]
  apply ZMod.castHom_injective

Bijectivity of the canonical homomorphism from $\mathbb{Z}/n\mathbb{Z}$ to a finite ring of cardinality $n$

Informal description

Let $R$ be a finite ring with cardinality $n$. Then the canonical ring homomorphism $\text{castHom} : \mathbb{Z}/n\mathbb{Z} \to R$ is bijective. That is, it is both injective and surjective.

ZMod.ringEquiv definition

[Fintype R] (h : Fintype.card R = n) : ZMod n ≃+* R

Full source

/-- The unique ring isomorphism between `ZMod n` and a ring `R`
of characteristic `n` and cardinality `n`. -/
noncomputable def ringEquiv [Fintype R] (h : Fintype.card R = n) : ZModZMod n ≃+* R :=
  RingEquiv.ofBijective _ (ZMod.castHom_bijective R h)

Ring isomorphism between $\mathbb{Z}/n\mathbb{Z}$ and a finite ring of cardinality $n$

Informal description

Given a finite ring $ R $ with cardinality $ n $, there exists a unique ring isomorphism between the integers modulo $ n $ ($ \mathbb{Z}/n\mathbb{Z} $) and $ R $. This isomorphism is constructed from the canonical ring homomorphism $ \text{castHom} : \mathbb{Z}/n\mathbb{Z} \to R $, which is bijective under these conditions.

ZMod.ringEquivOfPrime definition

[Fintype R] {p : ℕ} (hp : p.Prime) (hR : Fintype.card R = p) : ZMod p ≃+* R

Full source

/-- 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`. -/
noncomputable def ringEquivOfPrime [Fintype R] {p : ℕ} (hp : p.Prime) (hR : Fintype.card R = p) :
    ZModZMod p ≃+* R :=
  have : Nontrivial R := Fintype.one_lt_card_iff_nontrivial.1 (hR ▸ hp.one_lt)
  -- The following line exists as `charP_of_card_eq_prime` in `Mathlib.Algebra.CharP.CharAndCard`.
  have : CharP R p := (CharP.charP_iff_prime_eq_zero hp).2 (hR ▸ Nat.cast_card_eq_zero R)
  ZMod.ringEquiv R hR

Ring isomorphism between $\mathbb{Z}/p\mathbb{Z}$ and a finite ring of prime cardinality $p$

Informal description

Given a finite ring $ R $ with cardinality equal to a prime number $ p $, there exists a unique ring isomorphism between the integers modulo $ p $ ($ \mathbb{Z}/p\mathbb{Z} $) and $ R $. This isomorphism is constructed from the canonical ring homomorphism $ \text{castHom} : \mathbb{Z}/p\mathbb{Z} \to R $, which is bijective under these conditions.

ZMod.ringEquivOfPrime_eq_ringEquiv theorem

[Fintype R] {p : ℕ} [CharP R p] (hp : p.Prime) (hR : Fintype.card R = p) : ringEquivOfPrime R hp hR = ringEquiv R hR

Full source

@[simp]
lemma ringEquivOfPrime_eq_ringEquiv [Fintype R] {p : ℕ} [CharP R p] (hp : p.Prime)
    (hR : Fintype.card R = p) : ringEquivOfPrime R hp hR = ringEquiv R hR := rfl

Equality of prime-characteristic ring isomorphisms: $\mathrm{ringEquivOfPrime} = \mathrm{ringEquiv}$ for rings of prime order

Informal description

Let $R$ be a finite ring of characteristic $p$ (a prime number) with cardinality $p$. Then the ring isomorphism $\mathrm{ringEquivOfPrime}$ between $\mathbb{Z}/p\mathbb{Z}$ and $R$ coincides with the general ring isomorphism $\mathrm{ringEquiv}$ between $\mathbb{Z}/p\mathbb{Z}$ and $R$.

ZMod.ringEquivCongr definition

{m n : ℕ} (h : m = n) : ZMod m ≃+* ZMod n

Full source

/-- The identity between `ZMod m` and `ZMod n` when `m = n`, as a ring isomorphism. -/
def ringEquivCongr {m n : ℕ} (h : m = n) : ZModZMod m ≃+* ZMod n := by
  rcases m with - | m <;> rcases n with - | n
  · exact RingEquiv.refl _
  · exfalso
    exact n.succ_ne_zero h.symm
  · exfalso
    exact m.succ_ne_zero h
  · exact
      { finCongr h with
        map_mul' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.coe_cast, Fin.coe_mul, Fin.coe_mul, Fin.coe_cast, Fin.coe_cast, ← h]
        map_add' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.coe_cast, Fin.val_add, Fin.val_add, Fin.coe_cast, Fin.coe_cast, ← h] }

Ring isomorphism between $\mathbb{Z}/m\mathbb{Z}$ and $\mathbb{Z}/n\mathbb{Z}$ for $m = n$

Informal description

Given an equality $m = n$ between natural numbers, the function $\mathrm{ringEquivCongr}(h)$ defines a ring isomorphism between the integers modulo $m$ ($\mathbb{Z}/m\mathbb{Z}$) and the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$). Specifically: - When $m = n = 0$, it is the identity ring isomorphism on $\mathbb{Z}$. - When $m = n > 0$, it is the ring isomorphism induced by the equivalence $\mathrm{finCongr}(h)$ between $\mathrm{Fin}(m)$ and $\mathrm{Fin}(n)$, preserving both multiplication and addition modulo $m$ (or $n$). - The cases where one of $m$ or $n$ is zero and the other is positive are impossible due to the equality $m = n$.

ZMod.ringEquivCongr_refl theorem

(a : ℕ) : ringEquivCongr (rfl : a = a) = .refl _

Full source

@[simp] lemma ringEquivCongr_refl (a : ℕ) : ringEquivCongr (rfl : a = a) = .refl _ := by
  cases a <;> rfl

Identity Ring Isomorphism for $\mathbb{Z}/a\mathbb{Z}$ via Reflexivity

Informal description

For any natural number $a$, the ring isomorphism $\mathrm{ringEquivCongr}$ applied to the reflexivity proof $\mathrm{rfl} : a = a$ yields the identity ring isomorphism on $\mathbb{Z}/a\mathbb{Z}$.

ZMod.ringEquivCongr_refl_apply theorem

{a : ℕ} (x : ZMod a) : ringEquivCongr rfl x = x

Full source

lemma ringEquivCongr_refl_apply {a : ℕ} (x : ZMod a) : ringEquivCongr rfl x = x := by
  rw [ringEquivCongr_refl]
  rfl

Identity Action of Reflexive Ring Isomorphism on $\mathbb{Z}/a\mathbb{Z}$ Elements

Informal description

For any natural number $a$ and any element $x \in \mathbb{Z}/a\mathbb{Z}$, the ring isomorphism $\mathrm{ringEquivCongr}$ applied to the reflexivity proof $\mathrm{rfl} : a = a$ acts as the identity on $x$, i.e., $\mathrm{ringEquivCongr}(\mathrm{rfl})(x) = x$.

ZMod.ringEquivCongr_symm theorem

{a b : ℕ} (hab : a = b) : (ringEquivCongr hab).symm = ringEquivCongr hab.symm

Full source

lemma ringEquivCongr_symm {a b : ℕ} (hab : a = b) :
    (ringEquivCongr hab).symm = ringEquivCongr hab.symm := by
  subst hab
  cases a <;> rfl

Inverse of Ring Isomorphism Between $\mathbb{Z}/a\mathbb{Z}$ and $\mathbb{Z}/b\mathbb{Z}$ for $a = b$

Informal description

For any natural numbers $a$ and $b$ with $a = b$, the inverse of the ring isomorphism $\mathrm{ringEquivCongr}(hab) : \mathbb{Z}/a\mathbb{Z} \cong \mathbb{Z}/b\mathbb{Z}$ is equal to the ring isomorphism $\mathrm{ringEquivCongr}(hab.symm) : \mathbb{Z}/b\mathbb{Z} \cong \mathbb{Z}/a\mathbb{Z}$.

ZMod.ringEquivCongr_trans theorem

 {a b c : ℕ} (hab : a = b) (hbc : b = c) :
  (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr (hab.trans hbc)

Full source

lemma ringEquivCongr_trans {a b c : ℕ} (hab : a = b) (hbc : b = c) :
    (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr (hab.trans hbc) := by
  subst hab hbc
  cases a <;> rfl

Transitivity of Ring Isomorphism for $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural numbers $a$, $b$, and $c$ with equalities $a = b$ and $b = c$, the composition of the ring isomorphisms $\mathbb{Z}/a\mathbb{Z} \cong \mathbb{Z}/b\mathbb{Z}$ and $\mathbb{Z}/b\mathbb{Z} \cong \mathbb{Z}/c\mathbb{Z}$ is equal to the ring isomorphism $\mathbb{Z}/a\mathbb{Z} \cong \mathbb{Z}/c\mathbb{Z}$ induced by the equality $a = c$.

ZMod.ringEquivCongr_ringEquivCongr_apply theorem

 {a b c : ℕ} (hab : a = b) (hbc : b = c) (x : ZMod a) :
  ringEquivCongr hbc (ringEquivCongr hab x) = ringEquivCongr (hab.trans hbc) x

Full source

lemma ringEquivCongr_ringEquivCongr_apply {a b c : ℕ} (hab : a = b) (hbc : b = c) (x : ZMod a) :
    ringEquivCongr hbc (ringEquivCongr hab x) = ringEquivCongr (hab.trans hbc) x := by
  rw [← ringEquivCongr_trans hab hbc]
  rfl

Composition of Ring Isomorphisms for $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural numbers $a$, $b$, and $c$ with equalities $a = b$ and $b = c$, and for any element $x \in \mathbb{Z}/a\mathbb{Z}$, the composition of the ring isomorphisms $\mathbb{Z}/a\mathbb{Z} \cong \mathbb{Z}/b\mathbb{Z}$ and $\mathbb{Z}/b\mathbb{Z} \cong \mathbb{Z}/c\mathbb{Z}$ applied to $x$ is equal to the ring isomorphism $\mathbb{Z}/a\mathbb{Z} \cong \mathbb{Z}/c\mathbb{Z}$ applied to $x$ induced by the equality $a = c$. In other words, the following diagram commutes: \[ \begin{CD} \mathbb{Z}/a\mathbb{Z} @>\mathrm{ringEquivCongr}(hab)>> \mathbb{Z}/b\mathbb{Z} \\ @| @V\mathrm{ringEquivCongr}(hbc)VV \\ \mathbb{Z}/a\mathbb{Z} @>>\mathrm{ringEquivCongr}(hab.trans hbc)> \mathbb{Z}/c\mathbb{Z} \end{CD} \]

ZMod.ringEquivCongr_val theorem

{a b : ℕ} (h : a = b) (x : ZMod a) : ZMod.val ((ZMod.ringEquivCongr h) x) = ZMod.val x

Full source

lemma ringEquivCongr_val {a b : ℕ} (h : a = b) (x : ZMod a) :
    ZMod.val ((ZMod.ringEquivCongr h) x) = ZMod.val x := by
  subst h
  cases a <;> rfl

Preservation of Natural Representatives under Ring Isomorphism of $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural numbers $a$ and $b$ with $a = b$, and for any element $x \in \mathbb{Z}/a\mathbb{Z}$, the natural number representative of the image of $x$ under the ring isomorphism $\mathbb{Z}/a\mathbb{Z} \cong \mathbb{Z}/b\mathbb{Z}$ induced by $h$ is equal to the natural number representative of $x$ itself. In other words, the isomorphism preserves the natural number representatives of elements.

ZMod.ringEquivCongr_intCast theorem

{a b : ℕ} (h : a = b) (z : ℤ) : ZMod.ringEquivCongr h z = z

Full source

lemma ringEquivCongr_intCast {a b : ℕ} (h : a = b) (z : ℤ) :
    ZMod.ringEquivCongr h z = z := by
  subst h
  cases a <;> rfl

Integer Cast Preservation under Ring Isomorphism of $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural numbers $a$ and $b$ such that $a = b$, and for any integer $z$, the ring isomorphism $\mathrm{ringEquivCongr}(h)$ between $\mathbb{Z}/a\mathbb{Z}$ and $\mathbb{Z}/b\mathbb{Z}$ maps the integer $z$ to itself, i.e., $\mathrm{ringEquivCongr}(h)(z) = z$.

ZMod.val_eq_zero theorem

: ∀ {n : ℕ} (a : ZMod n), a.val = 0 ↔ a = 0

Full source

@[simp]
theorem val_eq_zero : ∀ {n : ℕ} (a : ZMod n), a.val = 0 ↔ a = 0
  | 0, _ => Int.natAbs_eq_zero
  | n + 1, a => by
    rw [Fin.ext_iff]
    exact Iff.rfl

Characterization of Zero in $\mathbb{Z}/n\mathbb{Z}$ via Natural Representative

Informal description

For any natural number $n$ and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative $\text{val}(a)$ is equal to $0$ if and only if $a$ is the zero element in $\mathbb{Z}/n\mathbb{Z}$.

ZMod.intCast_eq_intCast_iff theorem

(a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [ZMOD c]

Full source

theorem intCast_eq_intCast_iff (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [ZMOD c] :=
  CharP.intCast_eq_intCast (ZMod c) c

Equality in $\mathbb{Z}/c\mathbb{Z}$ iff Congruent Modulo $c$

Informal description

For any integers $a$ and $b$ and any natural number $c$, the images of $a$ and $b$ in $\mathbb{Z}/c\mathbb{Z}$ are equal if and only if $a$ is congruent to $b$ modulo $c$, i.e., $(a : \mathbb{Z}/c\mathbb{Z}) = (b : \mathbb{Z}/c\mathbb{Z}) \leftrightarrow a \equiv b \pmod{c}$.

ZMod.intCast_eq_intCast_iff' theorem

(a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a % c = b % c

Full source

theorem intCast_eq_intCast_iff' (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a % c = b % c :=
  ZMod.intCast_eq_intCast_iff a b c

Equality in $\mathbb{Z}/c\mathbb{Z}$ via Remainders: $(a : \mathbb{Z}/c\mathbb{Z}) = (b : \mathbb{Z}/c\mathbb{Z}) \leftrightarrow a \bmod c = b \bmod c$

Informal description

For any integers $a$ and $b$ and any natural number $c$, the images of $a$ and $b$ in $\mathbb{Z}/c\mathbb{Z}$ are equal if and only if the remainders of $a$ and $b$ when divided by $c$ are equal, i.e., $(a : \mathbb{Z}/c\mathbb{Z}) = (b : \mathbb{Z}/c\mathbb{Z}) \leftrightarrow a \bmod c = b \bmod c$.

ZMod.val_intCast theorem

{n : ℕ} (a : ℤ) [NeZero n] : ↑(a : ZMod n).val = a % n

Full source

theorem val_intCast {n : ℕ} (a : ℤ) [NeZero n] : ↑(a : ZMod n).val = a % n := by
  have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _
  have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)
  refine (Int.emod_eq_of_lt hle hlt).symm.trans ?_
  rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]

Natural Representative of Integer Modulo $n$ Equals Remainder: $\text{val}(a) = a \bmod n$

Informal description

For any nonzero natural number $n$ and any integer $a$, the natural number representative $\text{val}(a)$ of $a$ in $\mathbb{Z}/n\mathbb{Z}$ satisfies $\text{val}(a) = a \bmod n$ when viewed as an integer.

ZMod.natCast_eq_natCast_iff theorem

(a b c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [MOD c]

Full source

theorem natCast_eq_natCast_iff (a b c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [MOD c] := by
  simpa [Int.natCast_modEq_iff] using ZMod.intCast_eq_intCast_iff a b c

Equality in $\mathbb{Z}/c\mathbb{Z}$ iff Congruent Modulo $c$ for Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, the images of $a$ and $b$ in $\mathbb{Z}/c\mathbb{Z}$ are equal if and only if $a$ is congruent to $b$ modulo $c$, i.e., $(a : \mathbb{Z}/c\mathbb{Z}) = (b : \mathbb{Z}/c\mathbb{Z}) \leftrightarrow a \equiv b \pmod{c}$.

ZMod.natCast_eq_natCast_iff' theorem

(a b c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a % c = b % c

Full source

theorem natCast_eq_natCast_iff' (a b c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a % c = b % c :=
  ZMod.natCast_eq_natCast_iff a b c

Equality in $\mathbb{Z}/c\mathbb{Z}$ via Remainders Modulo $c$

Informal description

For any natural numbers $a$, $b$, and $c$, the images of $a$ and $b$ in $\mathbb{Z}/c\mathbb{Z}$ are equal if and only if the remainders of $a$ and $b$ modulo $c$ are equal, i.e., $(a : \mathbb{Z}/c\mathbb{Z}) = (b : \mathbb{Z}/c\mathbb{Z}) \leftrightarrow a \bmod c = b \bmod c$.

ZMod.intCast_zmod_eq_zero_iff_dvd theorem

(a : ℤ) (b : ℕ) : (a : ZMod b) = 0 ↔ (b : ℤ) ∣ a

Full source

theorem intCast_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) : (a : ZMod b) = 0 ↔ (b : ℤ) ∣ a := by
  rw [← Int.cast_zero, ZMod.intCast_eq_intCast_iff, Int.modEq_zero_iff_dvd]

Integer in $\mathbb{Z}/b\mathbb{Z}$ is Zero iff Divisible by $b$

Informal description

For any integer $a$ and natural number $b$, the image of $a$ in $\mathbb{Z}/b\mathbb{Z}$ is zero if and only if $b$ divides $a$ (as integers), i.e., $(a : \mathbb{Z}/b\mathbb{Z}) = 0 \leftrightarrow b \mid a$.

ZMod.intCast_eq_intCast_iff_dvd_sub theorem

(a b : ℤ) (c : ℕ) : (a : ZMod c) = ↑b ↔ ↑c ∣ b - a

Full source

theorem intCast_eq_intCast_iff_dvd_sub (a b : ℤ) (c : ℕ) : (a : ZMod c) = ↑b ↔ ↑c ∣ b - a := by
  rw [ZMod.intCast_eq_intCast_iff, Int.modEq_iff_dvd]

Equality in $\mathbb{Z}/c\mathbb{Z}$ via Divisibility of Difference

Informal description

For any integers $a$ and $b$ and any natural number $c$, the images of $a$ and $b$ in $\mathbb{Z}/c\mathbb{Z}$ are equal if and only if $c$ divides the difference $b - a$, i.e., $(a : \mathbb{Z}/c\mathbb{Z}) = (b : \mathbb{Z}/c\mathbb{Z}) \leftrightarrow c \mid (b - a)$.

ZMod.natCast_zmod_eq_zero_iff_dvd theorem

(a b : ℕ) : (a : ZMod b) = 0 ↔ b ∣ a

Full source

theorem natCast_zmod_eq_zero_iff_dvd (a b : ℕ) : (a : ZMod b) = 0 ↔ b ∣ a := by
  rw [← Nat.cast_zero, ZMod.natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd]

Natural Number in $\mathbb{Z}/b\mathbb{Z}$ is Zero iff Divisible by $b$

Informal description

For any natural numbers $a$ and $b$, the image of $a$ in $\mathbb{Z}/b\mathbb{Z}$ is zero if and only if $b$ divides $a$, i.e., $(a : \mathbb{Z}/b\mathbb{Z}) = 0 \leftrightarrow b \mid a$.

ZMod.coe_intCast theorem

(a : ℤ) : cast (a : ZMod n) = a % n

Full source

theorem coe_intCast (a : ℤ) : cast (a : ZMod n) = a % n := by
  cases n
  · rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]; rfl
  · rw [← val_intCast, val]; rfl

Canonical Map Preserves Integer Remainder Modulo $n$

Informal description

For any integer $a$ and natural number $n$, the canonical map from $\mathbb{Z}/n\mathbb{Z}$ to $\mathbb{Z}$ satisfies $\text{cast}(a \bmod n) = a \bmod n$.

ZMod.intCast_cast_add theorem

(x y : ZMod n) : (cast (x + y) : ℤ) = (cast x + cast y) % n

Full source

lemma intCast_cast_add (x y : ZMod n) : (cast (x + y) : ℤ) = (cast x + cast y) % n := by
  rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Integer Cast Preserves Addition Modulo $n$: $\text{cast}(x + y) \equiv \text{cast}(x) + \text{cast}(y) \ (\text{mod}\ n)$

Informal description

For any elements $x$ and $y$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the integer representation of their sum satisfies $\text{cast}(x + y) \equiv \text{cast}(x) + \text{cast}(y) \ (\text{mod}\ n)$.

ZMod.intCast_cast_mul theorem

(x y : ZMod n) : (cast (x * y) : ℤ) = cast x * cast y % n

Full source

lemma intCast_cast_mul (x y : ZMod n) : (cast (x * y) : ℤ) = cast x * cast y % n := by
  rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Integer Representation of Product in $\mathbb{Z}/n\mathbb{Z}$ Modulo $n$

Informal description

For any elements $x$ and $y$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the integer representation of their product satisfies $\text{cast}(x \cdot y) \equiv \text{cast}(x) \cdot \text{cast}(y) \ (\text{mod}\ n)$.

ZMod.intCast_cast_sub theorem

(x y : ZMod n) : (cast (x - y) : ℤ) = (cast x - cast y) % n

Full source

lemma intCast_cast_sub (x y : ZMod n) : (cast (x - y) : ℤ) = (cast x - cast y) % n := by
  rw [← ZMod.coe_intCast, Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Integer Cast Preserves Subtraction in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any elements $x$ and $y$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the integer representative of their difference satisfies $\text{cast}(x - y) \equiv (\text{cast}(x) - \text{cast}(y)) \mod n$.

ZMod.intCast_cast_neg theorem

(x : ZMod n) : (cast (-x) : ℤ) = -cast x % n

Full source

lemma intCast_cast_neg (x : ZMod n) : (cast (-x) : ℤ) = -cast x % n := by
  rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]

Negation Preserved Under Integer Cast in $\mathbb{Z}/n\mathbb{Z}$: $\text{cast}(-x) \equiv -\text{cast}(x) \pmod{n}$

Informal description

For any element $x$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the canonical integer representation of $-x$ is congruent modulo $n$ to the negation of the canonical integer representation of $x$. That is, $\text{cast}(-x) \equiv -\text{cast}(x) \pmod{n}$.

ZMod.val_neg_one theorem

(n : ℕ) : (-1 : ZMod n.succ).val = n

Full source

@[simp]
theorem val_neg_one (n : ℕ) : (-1 : ZMod n.succ).val = n := by
  dsimp [val, Fin.coe_neg]
  cases n
  · simp [Nat.mod_one]
  · dsimp [ZMod, ZMod.cast]
    rw [Fin.coe_neg_one]

Natural representative of $-1$ in $\mathbb{Z}/(n+1)\mathbb{Z}$ is $n$

Informal description

For any natural number $n$, the natural number representative of $-1$ in the integers modulo $n+1$ is equal to $n$, i.e., $\mathrm{val}(-1 : \mathbb{Z}/(n+1)\mathbb{Z}) = n$.

ZMod.cast_neg_one theorem

{R : Type*} [Ring R] (n : ℕ) : cast (-1 : ZMod n) = (n - 1 : R)

Full source

/-- `-1 : ZMod n` lifts to `n - 1 : R`. This avoids the characteristic assumption in `cast_neg`. -/
theorem cast_neg_one {R : Type*} [Ring R] (n : ℕ) : cast (-1 : ZMod n) = (n - 1 : R) := by
  rcases n with - | n
  · dsimp [ZMod, ZMod.cast]; simp
  · rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]

Canonical image of $-1$ in $\mathbb{Z}/n\mathbb{Z}$ is $n - 1$

Informal description

For any ring $ R $ and any natural number $ n $, the canonical map from the integers modulo $ n $ to $ R $ sends $-1$ to $ n - 1 $, i.e., $\text{cast}(-1 : \mathbb{Z}/n\mathbb{Z}) = n - 1$ in $ R $.

ZMod.cast_sub_one theorem

{R : Type*} [Ring R] {n : ℕ} (k : ZMod n) : (cast (k - 1 : ZMod n) : R) = (if k = 0 then (n : R) else cast k) - 1

Full source

theorem cast_sub_one {R : Type*} [Ring R] {n : ℕ} (k : ZMod n) :
    (cast (k - 1 : ZMod n) : R) = (if k = 0 then (n : R) else cast k) - 1 := by
  split_ifs with hk
  · rw [hk, zero_sub, ZMod.cast_neg_one]
  · cases n
    · dsimp [ZMod, ZMod.cast]
      rw [Int.cast_sub, Int.cast_one]
    · dsimp [ZMod, ZMod.cast, ZMod.val]
      rw [Fin.coe_sub_one, if_neg]
      · rw [Nat.cast_sub, Nat.cast_one]
        rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
      · exact hk

Canonical Image of $k-1$ in $\mathbb{Z}/n\mathbb{Z}$: $n-1$ when $k=0$, otherwise $\text{cast}(k)-1$

Informal description

Let $R$ be a ring and $n$ be a natural number. For any element $k$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the image of $k - 1$ under the canonical map to $R$ satisfies: \[ \text{cast}(k - 1) = \begin{cases} n - 1 & \text{if } k = 0, \\ \text{cast}(k) - 1 & \text{otherwise.} \end{cases} \]

ZMod.natCast_eq_iff theorem

(p : ℕ) (n : ℕ) (z : ZMod p) [NeZero p] : ↑n = z ↔ ∃ k, n = z.val + p * k

Full source

theorem natCast_eq_iff (p : ℕ) (n : ℕ) (z : ZMod p) [NeZero p] :
    ↑n = z ↔ ∃ k, n = z.val + p * k := by
  constructor
  · rintro rfl
    refine ⟨n / p, ?_⟩
    rw [val_natCast, Nat.mod_add_div]
  · rintro ⟨k, rfl⟩
    rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]

Natural Number Congruence Criterion in $\mathbb{Z}/p\mathbb{Z}$: $n \equiv z \pmod{p} \iff n = z.\mathrm{val} + p k$ for some $k$

Informal description

For any positive integer $p$ and natural number $n$, and for any element $z$ in the integers modulo $p$ ($\mathbb{Z}/p\mathbb{Z}$), the canonical image of $n$ in $\mathbb{Z}/p\mathbb{Z}$ equals $z$ if and only if there exists an integer $k$ such that $n = z.\mathrm{val} + p \cdot k$, where $z.\mathrm{val}$ is the smallest non-negative representative of $z$ in $\mathbb{N}$.

ZMod.intCast_eq_iff theorem

(p : ℕ) (n : ℤ) (z : ZMod p) [NeZero p] : ↑n = z ↔ ∃ k, n = z.val + p * k

Full source

theorem intCast_eq_iff (p : ℕ) (n : ℤ) (z : ZMod p) [NeZero p] :
    ↑n = z ↔ ∃ k, n = z.val + p * k := by
  constructor
  · rintro rfl
    refine ⟨n / p, ?_⟩
    rw [val_intCast, Int.emod_add_ediv]
  · rintro ⟨k, rfl⟩
    rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]

Integer Congruence Criterion in $\mathbb{Z}/p\mathbb{Z}$: $n \equiv z \pmod{p} \iff n = \mathrm{val}(z) + p k$ for some $k$

Informal description

For any positive integer $p$ and integer $n$, and for any element $z$ in the integers modulo $p$ ($\mathbb{Z}/p\mathbb{Z}$), the canonical image of $n$ in $\mathbb{Z}/p\mathbb{Z}$ equals $z$ if and only if there exists an integer $k$ such that $n = \mathrm{val}(z) + p \cdot k$, where $\mathrm{val}(z)$ is the smallest non-negative representative of $z$ in $\mathbb{N}$.

ZMod.intCast_mod theorem

(a : ℤ) (b : ℕ) : ((a % b : ℤ) : ZMod b) = (a : ZMod b)

Full source

@[push_cast, simp]
theorem intCast_mod (a : ℤ) (b : ℕ) : ((a % b : ℤ) : ZMod b) = (a : ZMod b) := by
  rw [ZMod.intCast_eq_intCast_iff]
  apply Int.mod_modEq

Equality of Integer Modulo Images in $\mathbb{Z}/b\mathbb{Z}$

Informal description

For any integer $a$ and natural number $b$, the image of $a \bmod b$ in $\mathbb{Z}/b\mathbb{Z}$ is equal to the image of $a$ in $\mathbb{Z}/b\mathbb{Z}$, i.e., $(a \bmod b : \mathbb{Z}/b\mathbb{Z}) = (a : \mathbb{Z}/b\mathbb{Z})$.

ZMod.ker_intCastAddHom theorem

(n : ℕ) : (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples (n : ℤ)

Full source

theorem ker_intCastAddHom (n : ℕ) :
    (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples (n : ℤ) := by
  ext
  rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
    intCast_zmod_eq_zero_iff_dvd]

Kernel of Integer-to-ZMod Homomorphism is Multiples of $n$

Informal description

For any natural number $n$, the kernel of the canonical additive monoid homomorphism from the integers $\mathbb{Z}$ to the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) is equal to the additive subgroup of $\mathbb{Z}$ generated by $n$, i.e., $\ker(\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}) = n\mathbb{Z}$.

ZMod.cast_injective_of_le theorem

{m n : ℕ} [nzm : NeZero m] (h : m ≤ n) : Function.Injective (@cast (ZMod n) _ m)

Full source

theorem cast_injective_of_le {m n : ℕ} [nzm : NeZero m] (h : m ≤ n) :
    Function.Injective (@cast (ZMod n) _ m) := by
  cases m with
  | zero => cases nzm; simp_all
  | succ m =>
    rintro ⟨x, hx⟩ ⟨y, hy⟩ f
    simp only [cast, val, natCast_eq_natCast_iff',
      Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f
    apply Fin.ext
    exact f

Injectivity of the canonical map $\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ when $m \leq n$ and $m \neq 0$

Informal description

Let $m$ and $n$ be natural numbers with $m \neq 0$. If $m \leq n$, then the canonical map $\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ is injective.

ZMod.cast_zmod_eq_zero_iff_of_le theorem

{m n : ℕ} [NeZero m] (h : m ≤ n) (a : ZMod m) : (cast a : ZMod n) = 0 ↔ a = 0

Full source

theorem cast_zmod_eq_zero_iff_of_le {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ZMod m) :
    (cast a : ZMod n) = 0 ↔ a = 0 := by
  rw [← ZMod.cast_zero (n := m)]
  exact Injective.eq_iff' (cast_injective_of_le h) rfl

Canonical Map from $\mathbb{Z}/m\mathbb{Z}$ to $\mathbb{Z}/n\mathbb{Z}$ Has Trivial Kernel When $m \leq n$ and $m \neq 0$

Informal description

Let $m$ and $n$ be natural numbers with $m \neq 0$, and suppose $m \leq n$. For any element $a$ of the integers modulo $m$ ($\mathbb{Z}/m\mathbb{Z}$), the canonical map $\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ sends $a$ to zero if and only if $a$ is zero in $\mathbb{Z}/m\mathbb{Z}$. In other words, $\operatorname{cast}(a) = 0$ in $\mathbb{Z}/n\mathbb{Z}$ if and only if $a = 0$ in $\mathbb{Z}/m\mathbb{Z}$.

ZMod.natCast_toNat theorem

(p : ℕ) : ∀ {z : ℤ} (_h : 0 ≤ z), (z.toNat : ZMod p) = z

Full source

@[simp]
theorem natCast_toNat (p : ℕ) : ∀ {z : ℤ} (_h : 0 ≤ z), (z.toNat : ZMod p) = z
  | (n : ℕ), _h => by simp only [Int.cast_natCast, Int.toNat_natCast]
  | Int.negSucc n, h => by simp at h

Equality of Integer and Natural Number Representatives in $\mathbb{Z}/p\mathbb{Z}$ for Non-Negative Integers

Informal description

For any natural number $p$ and any integer $z \geq 0$, the canonical map from $\mathbb{Z}$ to $\mathbb{Z}/p\mathbb{Z}$ sends $z$ to the same element as the natural number obtained by truncating $z$ to $\mathbb{N}$ via `Int.toNat`. In other words, $(z \mod p) = (\text{toNat}(z) \mod p)$.

ZMod.val_injective theorem

(n : ℕ) [NeZero n] : Function.Injective (val : ZMod n → ℕ)

Full source

theorem val_injective (n : ℕ) [NeZero n] : Function.Injective (val : ZMod n → ℕ) := by
  cases n
  · cases NeZero.ne 0 rfl
  intro a b h
  dsimp [ZMod]
  ext
  exact h

Injectivity of the Natural Representative Map on $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any positive integer $ n $, the function $\text{val} : \mathbb{Z}/n\mathbb{Z} \to \mathbb{N}$ that maps an element of the integers modulo $ n $ to its least non-negative representative is injective. In other words, if $\text{val}(a) = \text{val}(b)$ for $ a, b \in \mathbb{Z}/n\mathbb{Z} $, then $ a = b $.

ZMod.val_one_eq_one_mod theorem

(n : ℕ) : (1 : ZMod n).val = 1 % n

Full source

theorem val_one_eq_one_mod (n : ℕ) : (1 : ZMod n).val = 1 % n := by
  rw [← Nat.cast_one, val_natCast]

Natural Representative of One in $\mathbb{Z}/n\mathbb{Z}$ Equals One Modulo $n$

Informal description

For any natural number $n$, the natural number representative of the element $1$ in $\mathbb{Z}/n\mathbb{Z}$ is equal to $1$ modulo $n$, i.e., $\text{val}(1) = 1 \bmod n$.

ZMod.val_two_eq_two_mod theorem

(n : ℕ) : (2 : ZMod n).val = 2 % n

Full source

theorem val_two_eq_two_mod (n : ℕ) : (2 : ZMod n).val = 2 % n := by
  rw [← Nat.cast_two, val_natCast]

Natural Representative of Two in $\mathbb{Z}/n\mathbb{Z}$ Equals Two Modulo $n$

Informal description

For any natural number $n$, the natural number representative of the element $2$ in $\mathbb{Z}/n\mathbb{Z}$ is equal to $2$ modulo $n$, i.e., $\text{val}(2) = 2 \bmod n$.

ZMod.val_one theorem

(n : ℕ) [Fact (1 < n)] : (1 : ZMod n).val = 1

Full source

theorem val_one (n : ℕ) [Fact (1 < n)] : (1 : ZMod n).val = 1 := by
  rw [val_one_eq_one_mod]
  exact Nat.mod_eq_of_lt Fact.out

Natural Representative of One in $\mathbb{Z}/n\mathbb{Z}$ for $n > 1$

Informal description

For any natural number $n > 1$, the natural number representative of the element $1$ in $\mathbb{Z}/n\mathbb{Z}$ is equal to $1$, i.e., $\text{val}(1) = 1$.

ZMod.val_one'' theorem

: ∀ {n}, n ≠ 1 → (1 : ZMod n).val = 1

Full source

lemma val_one'' : ∀ {n}, n ≠ 1 → (1 : ZMod n).val = 1
  | 0, _ => rfl
  | 1, hn => by cases hn rfl
  | n + 2, _ =>
    haveI : Fact (1 < n + 2) := ⟨by simp⟩
    ZMod.val_one _

Natural Representative of One in $\mathbb{Z}/n\mathbb{Z}$ for $n \neq 1$

Informal description

For any natural number $n \neq 1$, the natural number representative of the element $1$ in $\mathbb{Z}/n\mathbb{Z}$ is equal to $1$, i.e., $\text{val}(1) = 1$.

ZMod.val_add theorem

{n : ℕ} [NeZero n] (a b : ZMod n) : (a + b).val = (a.val + b.val) % n

Full source

theorem val_add {n : ℕ} [NeZero n] (a b : ZMod n) : (a + b).val = (a.val + b.val) % n := by
  cases n
  · cases NeZero.ne 0 rfl
  · apply Fin.val_add

Natural Representative of Sum in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any positive integer $n$ and any elements $a, b$ in the ring of integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of the sum $a + b$ is equal to the sum of their representatives modulo $n$. That is, $\text{val}(a + b) = (\text{val}(a) + \text{val}(b)) \bmod n$.

ZMod.val_add_of_lt theorem

{n : ℕ} {a b : ZMod n} (h : a.val + b.val < n) : (a + b).val = a.val + b.val

Full source

theorem val_add_of_lt {n : ℕ} {a b : ZMod n} (h : a.val + b.val < n) :
    (a + b).val = a.val + b.val := by
  have : NeZero n := by constructor; rintro rfl; simp at h
  rw [ZMod.val_add, Nat.mod_eq_of_lt h]

Sum Representatives in $\mathbb{Z}/n\mathbb{Z}$ When Below Modulus

Informal description

For any natural number $n$ and elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), if the sum of their natural number representatives satisfies $a.\text{val} + b.\text{val} < n$, then the natural number representative of their sum is equal to the sum of their representatives, i.e., $(a + b).\text{val} = a.\text{val} + b.\text{val}$.

ZMod.val_add_val_of_le theorem

{n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) : a.val + b.val = (a + b).val + n

Full source

theorem 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 := by
  rw [val_add, Nat.add_mod_add_of_le_add_mod, Nat.mod_eq_of_lt (val_lt _),
    Nat.mod_eq_of_lt (val_lt _)]
  rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]

Sum of Representatives in $\mathbb{Z}/n\mathbb{Z}$ When Exceeding Modulus: $\text{val}(a) + \text{val}(b) = \text{val}(a + b) + n$

Informal description

For any positive integer $ n $ and any elements $ a, b $ in the ring of integers modulo $ n $ ($\mathbb{Z}/n\mathbb{Z}$), if the sum of their natural number representatives satisfies $ n \leq \text{val}(a) + \text{val}(b) $, then the sum of their representatives equals the representative of their sum plus $ n $. That is, \[ \text{val}(a) + \text{val}(b) = \text{val}(a + b) + n. \]

ZMod.val_add_of_le theorem

{n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) : (a + b).val = a.val + b.val - n

Full source

theorem 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 := by
  rw [val_add_val_of_le h]
  exact eq_tsub_of_add_eq rfl

Representative of Sum in $\mathbb{Z}/n\mathbb{Z}$ When Exceeding Modulus: $\text{val}(a + b) = \text{val}(a) + \text{val}(b) - n$

Informal description

For any positive integer $ n $ and any elements $ a, b $ in the ring of integers modulo $ n $ ($\mathbb{Z}/n\mathbb{Z}$), if the sum of their natural number representatives satisfies $ n \leq \text{val}(a) + \text{val}(b) $, then the natural number representative of their sum is given by \[ \text{val}(a + b) = \text{val}(a) + \text{val}(b) - n. \]

ZMod.val_add_le theorem

{n : ℕ} (a b : ZMod n) : (a + b).val ≤ a.val + b.val

Full source

theorem val_add_le {n : ℕ} (a b : ZMod n) : (a + b).val ≤ a.val + b.val := by
  cases n
  · simpa [ZMod.val] using Int.natAbs_add_le _ _
  · simpa [ZMod.val_add] using Nat.mod_le _ _

Sum of Representatives in $\mathbb{Z}/n\mathbb{Z}$ is Bounded by Their Sum

Informal description

For any natural number $n$ and any elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of the sum $a + b$ is less than or equal to the sum of their representatives, i.e., \[ \text{val}(a + b) \leq \text{val}(a) + \text{val}(b). \]

ZMod.val_mul theorem

{n : ℕ} (a b : ZMod n) : (a * b).val = a.val * b.val % n

Full source

theorem val_mul {n : ℕ} (a b : ZMod n) : (a * b).val = a.val * b.val % n := by
  cases n
  · rw [Nat.mod_zero]
    apply Int.natAbs_mul
  · apply Fin.val_mul

Product Representative in $\mathbb{Z}/n\mathbb{Z}$ Modulo $n$

Informal description

For any natural number $n$ and elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of the product $a \cdot b$ is equal to the product of their representatives modulo $n$, i.e., \[ \text{val}(a \cdot b) = (\text{val}(a) \cdot \text{val}(b)) \mod n. \]

ZMod.val_mul_le theorem

{n : ℕ} (a b : ZMod n) : (a * b).val ≤ a.val * b.val

Full source

theorem val_mul_le {n : ℕ} (a b : ZMod n) : (a * b).val ≤ a.val * b.val := by
  rw [val_mul]
  apply Nat.mod_le

Upper Bound on Product Representative in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $n$ and elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of the product $a \cdot b$ is less than or equal to the product of their representatives, i.e., \[ \text{val}(a \cdot b) \leq \text{val}(a) \cdot \text{val}(b). \]

ZMod.val_mul_of_lt theorem

{n : ℕ} {a b : ZMod n} (h : a.val * b.val < n) : (a * b).val = a.val * b.val

Full source

theorem val_mul_of_lt {n : ℕ} {a b : ZMod n} (h : a.val * b.val < n) :
    (a * b).val = a.val * b.val := by
  rw [val_mul]
  apply Nat.mod_eq_of_lt h

Exact Product Representative in $\mathbb{Z}/n\mathbb{Z}$ for Small Products

Informal description

For any natural number $n$ and elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), if the product of their natural number representatives satisfies $a.val \cdot b.val < n$, then the natural number representative of their product is exactly the product of their representatives, i.e., \[ \text{val}(a \cdot b) = \text{val}(a) \cdot \text{val}(b). \]

ZMod.val_mul_iff_lt theorem

{n : ℕ} [NeZero n] (a b : ZMod n) : (a * b).val = a.val * b.val ↔ a.val * b.val < n

Full source

theorem val_mul_iff_lt {n : ℕ} [NeZero n] (a b : ZMod n) :
    (a * b).val = a.val * b.val ↔ a.val * b.val < n := by
  constructor <;> intro h
  · rw [← h]; apply ZMod.val_lt
  · apply ZMod.val_mul_of_lt h

Exact Product Representative Condition in $\mathbb{Z}/n\mathbb{Z}$: $\text{val}(ab) = \text{val}(a)\text{val}(b) \leftrightarrow \text{val}(a)\text{val}(b) < n$

Informal description

For any nonzero natural number $n$ and elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of the product $a \cdot b$ equals the product of their representatives if and only if the product of their representatives is less than $n$. In other words: \[ \text{val}(a \cdot b) = \text{val}(a) \cdot \text{val}(b) \quad \Leftrightarrow \quad \text{val}(a) \cdot \text{val}(b) < n. \]

ZMod.nontrivial instance

(n : ℕ) [Fact (1 < n)] : Nontrivial (ZMod n)

Full source

instance nontrivial (n : ℕ) [Fact (1 < n)] : Nontrivial (ZMod n) :=
  ⟨⟨0, 1, fun h =>
      zero_ne_one <|
        calc
          0 = (0 : ZMod n).val := by rw [val_zero]
          _ = (1 : ZMod n).val := congr_arg ZMod.val h
          _ = 1 := val_one n
          ⟩⟩

Nontriviality of $\mathbb{Z}/n\mathbb{Z}$ for $n > 1$

Informal description

For any natural number $n > 1$, the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) form a nontrivial ring, meaning there exist at least two distinct elements in $\mathbb{Z}/n\mathbb{Z}$.

ZMod.nontrivial' instance

: Nontrivial (ZMod 0)

Full source

instance nontrivial' : Nontrivial (ZMod 0) := by
  delta ZMod; infer_instance

Nontriviality of Integers Modulo Zero

Informal description

The integers modulo 0, $\mathbb{Z}/0\mathbb{Z}$, form a nontrivial type, meaning they contain at least two distinct elements.

ZMod.one_eq_zero_iff theorem

{n : ℕ} : (1 : ZMod n) = 0 ↔ n = 1

Full source

lemma one_eq_zero_iff {n : ℕ} : (1 : ZMod n) = 0 ↔ n = 1 := by
  rw [← Nat.cast_one, natCast_zmod_eq_zero_iff_dvd, Nat.dvd_one]

Characterization of $\mathbb{Z}/n\mathbb{Z}$ where $1 = 0$

Informal description

For any natural number $n$, the multiplicative identity $1$ in the ring $\mathbb{Z}/n\mathbb{Z}$ is equal to the additive identity $0$ if and only if $n = 1$.

ZMod.inv definition

: ∀ n : ℕ, ZMod n → ZMod n

Full source

/-- 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`. -/
def inv : ∀ n : ℕ, ZMod n → ZMod n
  | 0, i => Int.sign i
  | n + 1, i => Nat.gcdA i.val (n + 1)

Inversion in $\mathbb{Z}/n\mathbb{Z}$

Informal description

The inversion operation on $\mathbb{Z}/n\mathbb{Z}$ is defined as: - For $n = 0$ (i.e., $\mathbb{Z}$), the inverse of $i$ is $\text{sign}(i)$ - For $n > 0$, the inverse of $i$ is given by the Bézout coefficient $a$ from $\gcd(i.\text{val}, n+1) = i.\text{val} \cdot a + (n+1) \cdot b$ This operation satisfies $a \cdot a^{-1} = \gcd(a.\text{val}, n)$. In particular, when $a$ is coprime to $n$, we have $a \cdot a^{-1} = 1$.

ZMod.instInv instance

(n : ℕ) : Inv (ZMod n)

Full source

instance (n : ℕ) : Inv (ZMod n) :=
  ⟨inv n⟩

Inversion Operation on Integers Modulo $ n $

Informal description

For any natural number $ n $, the integers modulo $ n $ ($\mathbb{Z}/n\mathbb{Z}$) have an inversion operation defined as follows: - When $ n = 0 $ (i.e., for $\mathbb{Z}$), the inverse of $ i $ is $\text{sign}(i)$. - When $ n > 0 $, the inverse of $ i $ is given by the Bézout coefficient $ a $ from the equation $\gcd(i.\text{val}, n+1) = i.\text{val} \cdot a + (n+1) \cdot b$. This operation satisfies $ a \cdot a^{-1} = \gcd(a.\text{val}, n) $. In particular, when $ a $ is coprime to $ n $, we have $ a \cdot a^{-1} = 1 $.

ZMod.inv_zero theorem

: ∀ n : ℕ, (0 : ZMod n)⁻¹ = 0

Full source

theorem inv_zero : ∀ n : ℕ, (0 : ZMod n)⁻¹ = 0
  | 0 => Int.sign_zero
  | n + 1 =>
    show (Nat.gcdA _ (n + 1) : ZMod (n + 1)) = 0 by
      rw [val_zero]
      unfold Nat.gcdA Nat.xgcd Nat.xgcdAux
      rfl

Inverse of Zero in $\mathbb{Z}/n\mathbb{Z}$ is Zero

Informal description

For any natural number $ n $, the multiplicative inverse of zero in the ring of integers modulo $ n $ is zero, i.e., $ 0^{-1} = 0 $ in $\mathbb{Z}/n\mathbb{Z}$.

ZMod.mul_inv_eq_gcd theorem

{n : ℕ} (a : ZMod n) : a * a⁻¹ = Nat.gcd a.val n

Full source

theorem mul_inv_eq_gcd {n : ℕ} (a : ZMod n) : a * a⁻¹ = Nat.gcd a.val n := by
  rcases n with - | n
  · dsimp [ZMod] at a ⊢
    calc
      _ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]
  · calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

Product of Element and Its Inverse in $\mathbb{Z}/n\mathbb{Z}$ Equals GCD of Representative and $ n $

Informal description

For any natural number $ n $ and any element $ a $ in the integers modulo $ n $ ($\mathbb{Z}/n\mathbb{Z}$), the product of $ a $ with its multiplicative inverse equals the greatest common divisor of the natural representative of $ a $ and $ n $. That is, \[ a \cdot a^{-1} = \gcd(a.\mathrm{val}, n). \]

ZMod.inv_one theorem

(n : ℕ) : (1⁻¹ : ZMod n) = 1

Full source

@[simp] protected lemma inv_one (n : ℕ) : (1⁻¹ : ZMod n) = 1 := by
  obtain rfl | hn := eq_or_ne n 1
  · exact Subsingleton.elim _ _
  · simpa [ZMod.val_one'' hn] using mul_inv_eq_gcd (1 : ZMod n)

Inverse of One in $\mathbb{Z}/n\mathbb{Z}$ is One

Informal description

For any natural number $n$, the multiplicative inverse of $1$ in the ring of integers modulo $n$ is $1$, i.e., $1^{-1} = 1$ in $\mathbb{Z}/n\mathbb{Z}$.

ZMod.natCast_mod theorem

(a : ℕ) (n : ℕ) : ((a % n : ℕ) : ZMod n) = a

Full source

@[simp]
theorem natCast_mod (a : ℕ) (n : ℕ) : ((a % n : ℕ) : ZMod n) = a := by
  conv =>
      rhs
      rw [← Nat.mod_add_div a n]
  simp

Congruence of Natural Number Modulo Reduction in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural numbers $a$ and $n$, the canonical map from $\mathbb{N}$ to $\mathbb{Z}/n\mathbb{Z}$ sends $a \bmod n$ to the same element as $a$ in $\mathbb{Z}/n\mathbb{Z}$. In other words, $(a \bmod n) \equiv a \pmod{n}$.

ZMod.ne_zero_iff_odd theorem

{n : ℕ} : (n : ZMod 2) ≠ 0 ↔ Odd n

Full source

theorem ne_zero_iff_odd {n : ℕ} : (n : ZMod 2) ≠ 0(n : ZMod 2) ≠ 0 ↔ Odd n := by
  constructor <;>
    · contrapose
      simp [eq_zero_iff_even]

Nonzero Modulo 2 iff Odd

Informal description

For any natural number $n$, the image of $n$ in $\mathbb{Z}/2\mathbb{Z}$ is nonzero if and only if $n$ is odd. In other words, $n \not\equiv 0 \pmod{2}$ if and only if $n$ is odd.

ZMod.coe_mul_inv_eq_one theorem

{n : ℕ} (x : ℕ) (h : Nat.Coprime x n) : ((x : ZMod n) * (x : ZMod n)⁻¹) = 1

Full source

theorem coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) :
    ((x : ZMod n) * (x : ZMod n)⁻¹) = 1 := by
  rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h
  rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]

Multiplicative Inverse Property in $\mathbb{Z}/n\mathbb{Z}$ for Coprime Elements

Informal description

For any natural numbers $n$ and $x$ such that $x$ is coprime with $n$, the product of $x$ with its multiplicative inverse in $\mathbb{Z}/n\mathbb{Z}$ equals $1$, i.e., \[ (x \bmod n) \cdot (x \bmod n)^{-1} \equiv 1 \pmod{n}. \]

ZMod.mul_val_inv theorem

(hmn : m.Coprime n) : (m * (m⁻¹ : ZMod n).val : ZMod n) = 1

Full source

lemma mul_val_inv (hmn : m.Coprime n) : (m * (m⁻¹ : ZMod n).val : ZMod n) = 1 := by
  obtain rfl | hn := eq_or_ne n 0
  · simp [m.coprime_zero_right.1 hmn]
  haveI : NeZero n := ⟨hn⟩
  rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]

Coprime Multiplicative Inverse Property in $\mathbb{Z}/n\mathbb{Z}$: $m \cdot (m^{-1}).\mathrm{val} \equiv 1 \pmod{n}$

Informal description

For any natural numbers $m$ and $n$ such that $m$ is coprime with $n$, the product of $m$ and the natural number representative of its multiplicative inverse in $\mathbb{Z}/n\mathbb{Z}$ equals $1$ in $\mathbb{Z}/n\mathbb{Z}$, i.e., \[ m \cdot (m^{-1}).\mathrm{val} \equiv 1 \pmod{n}. \]

ZMod.val_inv_mul theorem

(hmn : m.Coprime n) : ((m⁻¹ : ZMod n).val * m : ZMod n) = 1

Full source

lemma val_inv_mul (hmn : m.Coprime n) : ((m⁻¹ : ZMod n).val * m : ZMod n) = 1 := by
  rw [mul_comm, mul_val_inv hmn]

Multiplicative Inverse Property in $\mathbb{Z}/n\mathbb{Z}$: $(m^{-1}).\mathrm{val} \cdot m \equiv 1 \pmod{n}$

Informal description

For any natural numbers $m$ and $n$ such that $m$ is coprime with $n$, the product of the natural number representative of the multiplicative inverse of $m$ in $\mathbb{Z}/n\mathbb{Z}$ and $m$ equals $1$ in $\mathbb{Z}/n\mathbb{Z}$, i.e., \[ (m^{-1}).\mathrm{val} \cdot m \equiv 1 \pmod{n}. \]

ZMod.unitOfCoprime definition

{n : ℕ} (x : ℕ) (h : Nat.Coprime x n) : (ZMod n)ˣ

Full source

/-- `unitOfCoprime` makes an element of `(ZMod n)ˣ` given
a natural number `x` and a proof that `x` is coprime to `n` -/
def unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) : (ZMod n)ˣ :=
  ⟨x, x⁻¹, coe_mul_inv_eq_one x h, by rw [mul_comm, coe_mul_inv_eq_one x h]⟩

Unit construction from a coprime natural number in $\mathbb{Z}/n\mathbb{Z}$

Informal description

Given a natural number $ x $ and a proof that $ x $ is coprime to $ n $, the function `unitOfCoprime` constructs a unit in the ring $\mathbb{Z}/n\mathbb{Z}$ represented by $ x $. Specifically, it returns the pair $(x, x^{-1})$ where $ x^{-1} $ is the multiplicative inverse of $ x $ modulo $ n $, satisfying $ x \cdot x^{-1} \equiv 1 \pmod{n} $.

ZMod.coe_unitOfCoprime theorem

{n : ℕ} (x : ℕ) (h : Nat.Coprime x n) : (unitOfCoprime x h : ZMod n) = x

Full source

@[simp]
theorem coe_unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) :
    (unitOfCoprime x h : ZMod n) = x :=
  rfl

Canonical Embedding of Coprime Unit in $\mathbb{Z}/n\mathbb{Z}$ Equals Original Value

Informal description

For any natural numbers $x$ and $n$ such that $x$ is coprime with $n$, the canonical embedding of the unit $\mathrm{unitOfCoprime}(x, h)$ in $\mathbb{Z}/n\mathbb{Z}$ equals $x$ modulo $n$, i.e., $\mathrm{unitOfCoprime}(x, h) \equiv x \pmod{n}$.

ZMod.val_coe_unit_coprime theorem

{n : ℕ} (u : (ZMod n)ˣ) : Nat.Coprime (u : ZMod n).val n

Full source

theorem val_coe_unit_coprime {n : ℕ} (u : (ZMod n)ˣ) : Nat.Coprime (u : ZMod n).val n := by
  rcases n with - | n
  · rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp
  apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val
  have := Units.ext_iff.1 (mul_inv_cancel u)
  rw [Units.val_one] at this
  rw [← eq_iff_modEq_nat, Nat.cast_one, ← this]; clear this
  rw [← natCast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]
  rw [Units.val_mul, val_mul, natCast_mod]

Coprimality of Unit Representative in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $n$ and any unit $u$ in the ring $\mathbb{Z}/n\mathbb{Z}$, the natural number representative of $u$ (denoted by $u.\mathrm{val}$) is coprime with $n$, i.e., $\gcd(u.\mathrm{val}, n) = 1$.

ZMod.isUnit_iff_coprime theorem

(m n : ℕ) : IsUnit (m : ZMod n) ↔ m.Coprime n

Full source

lemma isUnit_iff_coprime (m n : ℕ) : IsUnitIsUnit (m : ZMod n) ↔ m.Coprime n := by
  refine ⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩
  have H' := val_coe_unit_coprime H.unit
  rw [IsUnit.unit_spec, val_natCast, Nat.coprime_iff_gcd_eq_one] at H'
  rw [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm, ← H']
  exact Nat.gcd_rec n m

Characterization of Units in $\mathbb{Z}/n\mathbb{Z}$ via Coprimality

Informal description

For any natural numbers $m$ and $n$, the element $m$ in the ring $\mathbb{Z}/n\mathbb{Z}$ is a unit if and only if $m$ and $n$ are coprime, i.e., $\gcd(m, n) = 1$.

ZMod.isUnit_prime_iff_not_dvd theorem

{n p : ℕ} (hp : p.Prime) : IsUnit (p : ZMod n) ↔ ¬p ∣ n

Full source

lemma isUnit_prime_iff_not_dvd {n p : ℕ} (hp : p.Prime) : IsUnitIsUnit (p : ZMod n) ↔ ¬p ∣ n := by
  rw [isUnit_iff_coprime, Nat.Prime.coprime_iff_not_dvd hp]

Characterization of Prime Units in $\mathbb{Z}/n\mathbb{Z}$: $p$ is a unit $\leftrightarrow p \nmid n$

Informal description

For any prime natural number $p$ and any natural number $n$, the element $p$ in the ring $\mathbb{Z}/n\mathbb{Z}$ is a unit if and only if $p$ does not divide $n$.

ZMod.isUnit_prime_of_not_dvd theorem

{n p : ℕ} (hp : p.Prime) (h : ¬p ∣ n) : IsUnit (p : ZMod n)

Full source

lemma isUnit_prime_of_not_dvd {n p : ℕ} (hp : p.Prime) (h : ¬ p ∣ n) : IsUnit (p : ZMod n) :=
  (isUnit_prime_iff_not_dvd hp).mpr h

Prime $p$ is a unit in $\mathbb{Z}/n\mathbb{Z}$ when $p \nmid n$

Informal description

For any prime natural number $p$ and any natural number $n$, if $p$ does not divide $n$, then $p$ is a unit in the ring $\mathbb{Z}/n\mathbb{Z}$.

ZMod.inv_coe_unit theorem

{n : ℕ} (u : (ZMod n)ˣ) : (u : ZMod n)⁻¹ = (u⁻¹ : (ZMod n)ˣ)

Full source

@[simp]
theorem inv_coe_unit {n : ℕ} (u : (ZMod n)ˣ) : (u : ZMod n)⁻¹ = (u⁻¹ : (ZMod n)ˣ) := by
  have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)
  rw [← mul_inv_eq_gcd, Nat.cast_one] at this
  let u' : (ZMod n)ˣ := ⟨u, (u : ZMod n)⁻¹, this, by rwa [mul_comm]⟩
  have h : u = u' := by
    apply Units.ext
    rfl
  rw [h]
  rfl

Inverse of Unit in $\mathbb{Z}/n\mathbb{Z}$ Equals Group Inverse

Informal description

For any natural number $n$ and any unit $u$ in the ring $\mathbb{Z}/n\mathbb{Z}$, the multiplicative inverse of the element $u$ in $\mathbb{Z}/n\mathbb{Z}$ equals the element corresponding to the inverse of $u$ in the group of units. That is, $$(u : \mathbb{Z}/n\mathbb{Z})^{-1} = (u^{-1} : (\mathbb{Z}/n\mathbb{Z})^\times).$$

ZMod.mul_inv_of_unit theorem

{n : ℕ} (a : ZMod n) (h : IsUnit a) : a * a⁻¹ = 1

Full source

theorem mul_inv_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) : a * a⁻¹ = 1 := by
  rcases h with ⟨u, rfl⟩
  rw [inv_coe_unit, u.mul_inv]

Unit Multiplication by Inverse Yields Identity in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $n$ and any element $a$ in the ring $\mathbb{Z}/n\mathbb{Z}$ that is a unit, the product of $a$ and its multiplicative inverse equals the multiplicative identity, i.e., $a \cdot a^{-1} = 1$.

ZMod.inv_mul_of_unit theorem

{n : ℕ} (a : ZMod n) (h : IsUnit a) : a⁻¹ * a = 1

Full source

theorem inv_mul_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) : a⁻¹ * a = 1 := by
  rw [mul_comm, mul_inv_of_unit a h]

Inverse Multiplication Identity for Units in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $n$ and any unit $a$ in the ring $\mathbb{Z}/n\mathbb{Z}$, the product of the multiplicative inverse of $a$ and $a$ equals the multiplicative identity, i.e., $a^{-1} \cdot a = 1$.

ZMod.inv_eq_of_mul_eq_one theorem

(n : ℕ) (a b : ZMod n) (h : a * b = 1) : a⁻¹ = b

Full source

protected theorem inv_eq_of_mul_eq_one (n : ℕ) (a b : ZMod n) (h : a * b = 1) : a⁻¹ = b :=
  left_inv_eq_right_inv (inv_mul_of_unit a ⟨⟨a, b, h, mul_comm a b ▸ h⟩, rfl⟩) h

Inverse Characterization via Multiplication Identity in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $n$ and elements $a, b$ in the ring $\mathbb{Z}/n\mathbb{Z}$, if $a \cdot b = 1$, then the multiplicative inverse of $a$ is equal to $b$, i.e., $a^{-1} = b$.

ZMod.inv_mul_eq_one_of_isUnit theorem

{n : ℕ} {a : ZMod n} (ha : IsUnit a) (b : ZMod n) : a⁻¹ * b = 1 ↔ a = b

Full source

lemma inv_mul_eq_one_of_isUnit {n : ℕ} {a : ZMod n} (ha : IsUnit a) (b : ZMod n) :
    a⁻¹a⁻¹ * b = 1 ↔ a = b := by
  -- ideally, this would be `ha.inv_mul_eq_one`, but `ZMod n` is not a `DivisionMonoid`...
  -- (see the "TODO" above)
  refine ⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩
  apply_fun (a * ·) at H
  rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H

Characterization of Units in $\mathbb{Z}/n\mathbb{Z}$ via Inverse Multiplication: $a^{-1}b = 1 \leftrightarrow a = b$

Informal description

For any natural number $n$ and any unit $a$ in the ring $\mathbb{Z}/n\mathbb{Z}$, and for any element $b \in \mathbb{Z}/n\mathbb{Z}$, the equation $a^{-1} \cdot b = 1$ holds if and only if $a = b$.

ZMod.unitsEquivCoprime definition

{n : ℕ} [NeZero n] : (ZMod n)ˣ ≃ { x : ZMod n // Nat.Coprime x.val n }

Full source

/-- Equivalence between the units of `ZMod n` and
the subtype of terms `x : ZMod n` for which `x.val` is coprime to `n` -/
def unitsEquivCoprime {n : ℕ} [NeZero n] : (ZMod n)ˣ(ZMod n)ˣ ≃ { x : ZMod n // Nat.Coprime x.val n } where
  toFun x := ⟨x, val_coe_unit_coprime x⟩
  invFun x := unitOfCoprime x.1.val x.2
  left_inv := fun ⟨_, _, _, _⟩ => Units.ext (natCast_zmod_val _)
  right_inv := fun ⟨_, _⟩ => by simp

Bijection between units of $\mathbb{Z}/n\mathbb{Z}$ and coprime elements

Informal description

For any nonzero natural number $ n $, there is a bijection between the group of units $ (\mathbb{Z}/n\mathbb{Z})^\times $ and the set of elements $ x \in \mathbb{Z}/n\mathbb{Z} $ for which the natural number representative $ x.\mathrm{val} $ is coprime to $ n $. The bijection is constructed as follows: 1. The forward map sends a unit $ u \in (\mathbb{Z}/n\mathbb{Z})^\times $ to the element $ u $ paired with a proof that $ u.\mathrm{val} $ is coprime to $ n $. 2. The inverse map takes an element $ x \in \mathbb{Z}/n\mathbb{Z} $ with $ \gcd(x.\mathrm{val}, n) = 1 $ and constructs the unit $ \mathrm{unitOfCoprime}(x.\mathrm{val}, \text{proof}) $, where $ \mathrm{unitOfCoprime} $ is the function that produces a unit from a coprime natural number. The maps are mutual inverses, establishing the equivalence.

ZMod.chineseRemainder definition

{m n : ℕ} (h : m.Coprime n) : ZMod (m * n) ≃+* ZMod m × ZMod n

Full source

/-- 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.
-/
def chineseRemainder {m n : ℕ} (h : m.Coprime n) : ZModZMod (m * n) ≃+* ZMod m × ZMod n :=
  let to_fun : ZMod (m * n) → ZModZMod m × ZMod n :=
    ZMod.castHom (show m.lcm n ∣ m * n by simp [Nat.lcm_dvd_iff]) (ZModZMod m × ZMod n)
  let inv_fun : ZModZMod m × ZMod n → ZMod (m * n) := fun x =>
    if m * n = 0 then
      if m = 1 then cast (RingHom.snd _ (ZMod n) x) else cast (RingHom.fst (ZMod m) _ x)
    else Nat.chineseRemainder h x.1.val x.2.val
  have inv : Function.LeftInverseFunction.LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun :=
    if hmn0 : m * n = 0 then by
      rcases h.eq_of_mul_eq_zero hmn0 with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
      · constructor
        · intro x; rfl
        · rintro ⟨x, y⟩
          fin_cases y
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]
      · constructor
        · intro x; rfl
        · rintro ⟨x, y⟩
          fin_cases x
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]
    else by
      haveI : NeZero (m * n) := ⟨hmn0⟩
      haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
      haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
      have left_inv : Function.LeftInverse inv_fun to_fun := by
        intro x
        dsimp only [to_fun, inv_fun, ZMod.castHom_apply]
        conv_rhs => rw [← ZMod.natCast_zmod_val x]
        rw [if_neg hmn0, ZMod.eq_iff_modEq_nat, ← Nat.modEq_and_modEq_iff_modEq_mul h,
          Prod.fst_zmod_cast, Prod.snd_zmod_cast]
        refine
          ⟨(Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.left.trans ?_,
            (Nat.chineseRemainder h (cast x : ZMod m).val (cast x : ZMod n).val).2.right.trans ?_⟩
        · rw [← ZMod.eq_iff_modEq_nat, ZMod.natCast_zmod_val, ZMod.natCast_val]
        · rw [← ZMod.eq_iff_modEq_nat, ZMod.natCast_zmod_val, ZMod.natCast_val]
      exact ⟨left_inv, left_inv.rightInverse_of_card_le (by simp)⟩
  { toFun := to_fun,
    invFun := inv_fun,
    map_mul' := RingHom.map_mul _
    map_add' := RingHom.map_add _
    left_inv := inv.1
    right_inv := inv.2 }

Chinese Remainder Theorem for Integers Modulo Coprime Numbers

Informal description

Given coprime natural numbers $ m $ and $ n $, the Chinese remainder theorem provides a ring isomorphism between the integers modulo $ m \times n $ ($ \mathbb{Z}/mn\mathbb{Z} $) and the direct product of the integers modulo $ m $ and modulo $ n $ ($ \mathbb{Z}/m\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z} $). The isomorphism is constructed as follows: 1. The forward map $ \text{to\_fun} : \mathbb{Z}/mn\mathbb{Z} \to \mathbb{Z}/m\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z} $ is the canonical ring homomorphism induced by the projections modulo $ m $ and $ n $. 2. The inverse map $ \text{inv\_fun} : \mathbb{Z}/m\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}/mn\mathbb{Z} $ is defined using the natural number solution to the simultaneous congruences $ k \equiv a \pmod{m} $ and $ k \equiv b \pmod{n} $ provided by the extended GCD algorithm, where $ a $ and $ b $ are the natural number representatives of the input elements. The maps are mutual inverses and preserve the ring structure (addition and multiplication).

ZMod.subsingleton_iff theorem

{n : ℕ} : Subsingleton (ZMod n) ↔ n = 1

Full source

lemma subsingleton_iff {n : ℕ} : SubsingletonSubsingleton (ZMod n) ↔ n = 1 := by
  constructor
  · obtain (_ | _ | n) := n
    · simpa [ZMod] using not_subsingleton _
    · simp [ZMod]
    · simpa [ZMod] using not_subsingleton _
  · rintro rfl
    infer_instance

Subsingleton Property of $\mathbb{Z}/n\mathbb{Z}$: $\mathrm{Subsingleton}(\mathbb{Z}/n\mathbb{Z}) \leftrightarrow n = 1$

Informal description

For any natural number $n$, the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) form a subsingleton (i.e., have at most one element) if and only if $n = 1$.

ZMod.nontrivial_iff theorem

{n : ℕ} : Nontrivial (ZMod n) ↔ n ≠ 1

Full source

lemma nontrivial_iff {n : ℕ} : NontrivialNontrivial (ZMod n) ↔ n ≠ 1 := by
  rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

Nontriviality of $\mathbb{Z}/n\mathbb{Z}$: $\text{Nontrivial}(\mathbb{Z}/n\mathbb{Z}) \leftrightarrow n \neq 1$

Informal description

For any natural number $n$, the ring $\mathbb{Z}/n\mathbb{Z}$ is nontrivial (contains at least two distinct elements) if and only if $n \neq 1$.

ZMod.subsingleton_units instance

: Subsingleton (ZMod 2)ˣ

Full source

instance subsingleton_units : Subsingleton (ZMod 2)ˣ :=
  ⟨by decide⟩

Uniqueness of Units in $\mathbb{Z}/2\mathbb{Z}$

Informal description

The group of units of the ring $\mathbb{Z}/2\mathbb{Z}$ is a subsingleton (i.e., has at most one element).

ZMod.add_self_eq_zero_iff_eq_zero theorem

{n : ℕ} (hn : Odd n) {a : ZMod n} : a + a = 0 ↔ a = 0

Full source

@[simp]
theorem add_self_eq_zero_iff_eq_zero {n : ℕ} (hn : Odd n) {a : ZMod n} :
    a + a = 0 ↔ a = 0 := by
  rw [Nat.odd_iff, ← Nat.two_dvd_ne_zero, ← Nat.prime_two.coprime_iff_not_dvd] at hn
  rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]

Characterization of Zero in $\mathbb{Z}/n\mathbb{Z}$ for Odd $n$: $2a = 0 \leftrightarrow a = 0$

Informal description

For any natural number $n$ such that $n$ is odd, and for any element $a$ in the ring $\mathbb{Z}/n\mathbb{Z}$, the equation $a + a = 0$ holds if and only if $a = 0$.

ZMod.ne_neg_self theorem

{n : ℕ} (hn : Odd n) {a : ZMod n} (ha : a ≠ 0) : a ≠ -a

Full source

theorem ne_neg_self {n : ℕ} (hn : Odd n) {a : ZMod n} (ha : a ≠ 0) : a ≠ -a := by
  rwa [Ne, eq_neg_iff_add_eq_zero, add_self_eq_zero_iff_eq_zero hn]

Nonzero Elements in $\mathbb{Z}/n\mathbb{Z}$ for Odd $n$ Are Not Self-Inverse

Informal description

For any natural number $n$ such that $n$ is odd, and for any nonzero element $a$ in the ring $\mathbb{Z}/n\mathbb{Z}$, $a$ is not equal to its additive inverse $-a$.

ZMod.neg_one_ne_one theorem

{n : ℕ} [Fact (2 < n)] : (-1 : ZMod n) ≠ 1

Full source

theorem neg_one_ne_one {n : ℕ} [Fact (2 < n)] : (-1 : ZMod n) ≠ 1 :=
  CharP.neg_one_ne_one (ZMod n) n

Negation of Unity in $\mathbb{Z}/n\mathbb{Z}$ for $n > 2$

Informal description

For any integer $n > 2$, the elements $-1$ and $1$ in the ring $\mathbb{Z}/n\mathbb{Z}$ are distinct, i.e., $-1 \neq 1$.

ZMod.neg_eq_self_mod_two theorem

(a : ZMod 2) : -a = a

Full source

@[simp]
theorem neg_eq_self_mod_two (a : ZMod 2) : -a = a := by
  fin_cases a <;> apply Fin.ext <;> simp [Fin.coe_neg, Int.natMod]; rfl

Negation in $\mathbb{Z}/2\mathbb{Z}$ is the Identity

Informal description

For any element $a$ in the integers modulo 2 ($\mathbb{Z}/2\mathbb{Z}$), the negation of $a$ is equal to $a$ itself, i.e., $-a = a$.

ZMod.natAbs_mod_two theorem

(a : ℤ) : (a.natAbs : ZMod 2) = a

Full source

@[simp]
theorem natAbs_mod_two (a : ℤ) : (a.natAbs : ZMod 2) = a := by
  cases a
  · simp only [Int.natAbs_natCast, Int.cast_natCast, Int.ofNat_eq_coe]
  · simp only [neg_eq_self_mod_two, Nat.cast_succ, Int.natAbs, Int.cast_negSucc]

Absolute Value Modulo Two Equals Original Modulo Two

Informal description

For any integer $a$, the natural number absolute value of $a$ modulo 2 is equal to $a$ modulo 2, i.e., $(|a| : \mathbb{Z}/2\mathbb{Z}) = a \bmod 2$.

ZMod.val_ne_zero theorem

{n : ℕ} (a : ZMod n) : a.val ≠ 0 ↔ a ≠ 0

Full source

theorem val_ne_zero {n : ℕ} (a : ZMod n) : a.val ≠ 0a.val ≠ 0 ↔ a ≠ 0 :=
  (val_eq_zero a).not

Nonzero Natural Representative Characterizes Nonzero Elements in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $n$ and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative $\text{val}(a)$ is nonzero if and only if $a$ is not the zero element in $\mathbb{Z}/n\mathbb{Z}$.

ZMod.val_pos theorem

{n : ℕ} {a : ZMod n} : 0 < a.val ↔ a ≠ 0

Full source

theorem val_pos {n : ℕ} {a : ZMod n} : 0 < a.val ↔ a ≠ 0 := by
  simp [pos_iff_ne_zero]

Positivity of Natural Representative in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $n$ and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative $\text{val}(a)$ is positive if and only if $a$ is not zero. In other words, $0 < \text{val}(a) \leftrightarrow a \neq 0$.

ZMod.val_eq_one theorem

: ∀ {n : ℕ} (_ : 1 < n) (a : ZMod n), a.val = 1 ↔ a = 1

Full source

theorem val_eq_one : ∀ {n : ℕ} (_ : 1 < n) (a : ZMod n), a.val = 1 ↔ a = 1
  | 0, hn, _
  | 1, hn, _ => by simp at hn
  | n + 2, _, _ => by simp only [val, ZMod, Fin.ext_iff, Fin.val_one]

Natural Representative Equals One if and only if Congruent to One Modulo $n$

Informal description

For any integer $a$ modulo $n$ (where $n > 1$), the natural number representative of $a$ equals $1$ if and only if $a$ is congruent to $1$ modulo $n$, i.e., $a \equiv 1 \pmod{n}$.

ZMod.neg_eq_self_iff theorem

{n : ℕ} (a : ZMod n) : -a = a ↔ a = 0 ∨ 2 * a.val = n

Full source

theorem neg_eq_self_iff {n : ℕ} (a : ZMod n) : -a = a ↔ a = 0 ∨ 2 * a.val = n := by
  rw [neg_eq_iff_add_eq_zero, ← two_mul]
  cases n
  · rw [@mul_eq_zero ℤ, @mul_eq_zero ℕ, val_eq_zero]
    exact
      ⟨fun h => h.elim (by simp) Or.inl, fun h =>
        Or.inr (h.elim id fun h => h.elim (by simp) id)⟩
  conv_lhs =>
    rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_zmod_eq_zero_iff_dvd]
  constructor
  · rintro ⟨m, he⟩
    rcases m with - | m
    · rw [mul_zero, mul_eq_zero] at he
      rcases he with (⟨⟨⟩⟩ | he)
      exact Or.inl (a.val_eq_zero.1 he)
    cases m
    · right
      rwa [show 0 + 1 = 1 from rfl, mul_one] at he
    refine (a.val_lt.not_le <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim
    rw [he, mul_comm]
    apply Nat.mul_le_mul_left
    simp
  · rintro (rfl | h)
    · rw [val_zero, mul_zero]
      apply dvd_zero
    · rw [h]

Negation Equals Self in $\mathbb{Z}/n\mathbb{Z}$ iff Zero or Twice Representative Equals $n$

Informal description

For any natural number $n$ and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the negation of $a$ equals $a$ itself if and only if either $a$ is zero or twice the natural representative of $a$ equals $n$, i.e., $-a = a \leftrightarrow (a = 0 \lor 2 \cdot \text{val}(a) = n)$.

ZMod.val_cast_of_lt theorem

{n : ℕ} {a : ℕ} (h : a < n) : (a : ZMod n).val = a

Full source

theorem val_cast_of_lt {n : ℕ} {a : ℕ} (h : a < n) : (a : ZMod n).val = a := by
  rw [val_natCast, Nat.mod_eq_of_lt h]

Natural Representative of Integer Modulo $n$ Equals Itself When Less Than $n$

Informal description

For any natural numbers $n$ and $a$ such that $a < n$, the natural number representative of the integer $a$ in $\mathbb{Z}/n\mathbb{Z}$ is equal to $a$ itself, i.e., $\text{val}(a \bmod n) = a$.

ZMod.val_cast_zmod_lt theorem

{m : ℕ} [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m) : (a.cast : ZMod n).val < m

Full source

theorem val_cast_zmod_lt {m : ℕ} [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m) :
    (a.cast : ZMod n).val < m := by
  rcases m with (⟨⟩|⟨m⟩); · cases NeZero.ne 0 rfl
  by_cases h : m < n
  · rcases n with (⟨⟩|⟨n⟩); · simp at h
    rw [← natCast_val, val_cast_of_lt]
    · apply a.val_lt
    apply lt_of_le_of_lt (Nat.le_of_lt_succ (ZMod.val_lt a)) h
  · rw [not_lt] at h
    apply lt_of_lt_of_le (ZMod.val_lt _) (le_trans h (Nat.le_succ m))

Bound on Natural Representative of Cast Element in $\mathbb{Z}/n\mathbb{Z}$: $\text{val}(a \bmod n) < m$

Informal description

For any nonzero natural numbers $m$ and $n$, and any element $a$ in the integers modulo $m$ ($\mathbb{Z}/m\mathbb{Z}$), the natural number representative of the image of $a$ under the canonical map to $\mathbb{Z}/n\mathbb{Z}$ is strictly less than $m$, i.e., $\text{val}(a \bmod n) < m$.

ZMod.neg_val' theorem

{n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = (n - a.val) % n

Full source

theorem neg_val' {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = (n - a.val) % n :=
  calc
    (-a).val = val (-a) % n := by rw [Nat.mod_eq_of_lt (-a).val_lt]
    _ = (n - val a) % n :=
      Nat.ModEq.add_right_cancel' (val a)
        (by
          rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero])

Natural Representative of Additive Inverse in $\mathbb{Z}/n\mathbb{Z}$: $(-a).\text{val} = (n - a.\text{val}) \bmod n$

Informal description

For any nonzero natural number $n$ and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of the additive inverse $-a$ is given by $(n - \text{val}(a)) \bmod n$, where $\text{val}(a)$ is the least natural number representative of $a$.

ZMod.neg_val theorem

{n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = if a = 0 then 0 else n - a.val

Full source

theorem neg_val {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = if a = 0 then 0 else n - a.val := by
  rw [neg_val']
  by_cases h : a = 0; · rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
  rw [if_neg h]
  apply Nat.mod_eq_of_lt
  apply Nat.sub_lt (NeZero.pos n)
  contrapose! h
  rwa [Nat.le_zero, val_eq_zero] at h

Natural Representative of Additive Inverse in $\mathbb{Z}/n\mathbb{Z}$: $\text{val}(-a) = n - \text{val}(a)$ for $a \neq 0$

Informal description

For any nonzero natural number $n$ and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of the additive inverse $-a$ is given by: \[ \text{val}(-a) = \begin{cases} 0 & \text{if } a = 0, \\ n - \text{val}(a) & \text{otherwise}, \end{cases} \] where $\text{val}(a)$ denotes the least natural number representative of $a$ in $\mathbb{Z}/n\mathbb{Z}$.

ZMod.val_neg_of_ne_zero theorem

{n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a] : (-a).val = n - a.val

Full source

theorem val_neg_of_ne_zero {n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a] :
    (- a).val = n - a.val := by simp_all [neg_val a, na.out]

Natural Representative of Additive Inverse for Nonzero Elements in $\mathbb{Z}/n\mathbb{Z}$: $\text{val}(-a) = n - \text{val}(a)$

Informal description

For any nonzero natural number $n$ and any nonzero element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of the additive inverse $-a$ satisfies $\text{val}(-a) = n - \text{val}(a)$, where $\text{val}(a)$ is the least natural number in the equivalence class of $a$.

ZMod.val_sub theorem

{n : ℕ} [NeZero n] {a b : ZMod n} (h : b.val ≤ a.val) : (a - b).val = a.val - b.val

Full source

theorem val_sub {n : ℕ} [NeZero n] {a b : ZMod n} (h : b.val ≤ a.val) :
    (a - b).val = a.val - b.val := by
  by_cases hb : b = 0
  · cases hb; simp
  · have : NeZero b := ⟨hb⟩
    rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
      add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]
    apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))

Natural Representative of Difference in $\mathbb{Z}/n\mathbb{Z}$ When $\text{val}(b) \leq \text{val}(a)$

Informal description

For any nonzero natural number $n$ and any elements $a, b$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), if the natural number representative of $b$ is less than or equal to that of $a$ (i.e., $\text{val}(b) \leq \text{val}(a)$), then the natural number representative of their difference satisfies $\text{val}(a - b) = \text{val}(a) - \text{val}(b)$.

ZMod.val_cast_eq_val_of_lt theorem

{m n : ℕ} [nzm : NeZero m] {a : ZMod m} (h : a.val < n) : (a.cast : ZMod n).val = a.val

Full source

theorem val_cast_eq_val_of_lt {m n : ℕ} [nzm : NeZero m] {a : ZMod m}
    (h : a.val < n) : (a.cast : ZMod n).val = a.val := by
  have nzn : NeZero n := by constructor; rintro rfl; simp at h
  cases m with
  | zero => cases nzm; simp_all
  | succ m =>
    cases n with
    | zero => cases nzn; simp_all
    | succ n => exact Fin.val_cast_of_lt h

Preservation of Natural Representative Under Casting in $\mathbb{Z}/n\mathbb{Z}$ When Less Than Modulus

Informal description

For any positive integers $ m $ and $ n $, and any element $ a $ of the integers modulo $ m $ ($\mathbb{Z}/m\mathbb{Z}$), if the natural number representative $ a.\text{val} $ of $ a $ is less than $ n $, then the natural number representative of the cast of $ a $ into $\mathbb{Z}/n\mathbb{Z}$ is equal to $ a.\text{val} $.

ZMod.cast_cast_zmod_of_le theorem

{m n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) : (cast (cast a : ZMod n) : ZMod m) = a

Full source

theorem cast_cast_zmod_of_le {m n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) :
    (cast (cast a : ZMod n) : ZMod m) = a := by
  have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩
  rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]

Double Casting Identity for $\mathbb{Z}/m\mathbb{Z}$ and $\mathbb{Z}/n\mathbb{Z}$ when $ m \leq n $

Informal description

For any positive integers $ m $ and $ n $ such that $ m \leq n $, and any element $ a $ in the integers modulo $ m $ ($\mathbb{Z}/m\mathbb{Z}$), the double casting of $ a $ through $\mathbb{Z}/n\mathbb{Z}$ back to $\mathbb{Z}/m\mathbb{Z}$ equals $ a $. That is, $\operatorname{cast}(\operatorname{cast}(a) : \mathbb{Z}/n\mathbb{Z}) : \mathbb{Z}/m\mathbb{Z} = a$.

ZMod.val_pow theorem

{m n : ℕ} {a : ZMod n} [ilt : Fact (1 < n)] (h : a.val ^ m < n) : (a ^ m).val = a.val ^ m

Full source

theorem val_pow {m n : ℕ} {a : ZMod n} [ilt : Fact (1 < n)] (h : a.val ^ m < n) :
    (a ^ m).val = a.val ^ m := by
  induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    have : a.val ^ m < n := by
      obtain rfl | ha := eq_or_ne a 0
      · by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]
      · exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h
    rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]

Power Representative Identity in $\mathbb{Z}/n\mathbb{Z}$ for Small Exponents

Informal description

For any natural numbers $m$ and $n > 1$, and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), if the $m$-th power of the natural number representative $\text{val}(a)$ is less than $n$, then the natural number representative of $a^m$ equals $\text{val}(a)^m$, i.e., \[ \text{val}(a^m) = \text{val}(a)^m. \]

ZMod.val_pow_le theorem

{m n : ℕ} [Fact (1 < n)] {a : ZMod n} : (a ^ m).val ≤ a.val ^ m

Full source

theorem val_pow_le {m n : ℕ} [Fact (1 < n)] {a : ZMod n} : (a ^ m).val ≤ a.val ^ m := by
  induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    rw [pow_succ, pow_succ]
    apply le_trans (ZMod.val_mul_le _ _)
    apply Nat.mul_le_mul_right _ ih

Upper Bound on Power Representative in $\mathbb{Z}/n\mathbb{Z}$ for $n > 1$

Informal description

For any natural numbers $m$ and $n > 1$, and any element $a$ in the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$), the natural number representative of $a^m$ is less than or equal to the $m$-th power of the representative of $a$, i.e., \[ \text{val}(a^m) \leq (\text{val}(a))^m. \]

ZMod.natAbs_min_of_le_div_two theorem

(n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (hl : x.natAbs ≤ n / 2) : x.natAbs ≤ y.natAbs

Full source

theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (hl : x.natAbs ≤ n / 2) :
    x.natAbs ≤ y.natAbs := by
  rw [intCast_eq_intCast_iff_dvd_sub] at he
  obtain ⟨m, he⟩ := he
  rw [sub_eq_iff_eq_add] at he
  subst he
  obtain rfl | hm := eq_or_ne m 0
  · rw [mul_zero, zero_add]
  apply hl.trans
  rw [← add_le_add_iff_right x.natAbs]
  refine le_trans (le_trans ((add_le_add_iff_left _).2 hl) ?_) (Int.natAbs_sub_le _ _)
  rw [add_sub_cancel_right, Int.natAbs_mul, Int.natAbs_natCast]
  refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
  rw [← mul_two]; apply Nat.div_mul_le_self

Minimal Representative Bound in $\mathbb{Z}/n\mathbb{Z}$: $|x| \leq n/2$ implies $|x| \leq |y|$ for congruent $y$

Informal description

For any natural number $n$ and integers $x$ and $y$ such that $x \equiv y \pmod{n}$ and the natural absolute value of $x$ satisfies $|x| \leq n/2$, we have $|x| \leq |y|$.

RingHom.ext_zmod theorem

{n : ℕ} {R : Type*} [NonAssocSemiring R] (f g : ZMod n →+* R) : f = g

Full source

theorem RingHom.ext_zmod {n : ℕ} {R : Type*} [NonAssocSemiring R] (f g : ZModZMod n →+* R) : f = g := by
  ext a
  obtain ⟨k, rfl⟩ := ZMod.intCast_surjective a
  let φ : ℤℤ →+* R := f.comp (Int.castRingHom (ZMod n))
  let ψ : ℤℤ →+* R := g.comp (Int.castRingHom (ZMod n))
  show φ k = ψ k
  rw [φ.ext_int ψ]

Uniqueness of Ring Homomorphisms from $\mathbb{Z}/n\mathbb{Z}$ to a Non-Associative Semiring

Informal description

Let $n$ be a natural number and $R$ be a non-associative semiring. For any two ring homomorphisms $f, g \colon \mathbb{Z}/n\mathbb{Z} \to R$, we have $f = g$.

ZMod.subsingleton_ringHom instance

[Semiring R] : Subsingleton (ZMod n →+* R)

Full source

instance subsingleton_ringHom [Semiring R] : Subsingleton (ZModZMod n →+* R) :=
  ⟨RingHom.ext_zmod⟩

Uniqueness of Ring Homomorphisms from $\mathbb{Z}/n\mathbb{Z}$ to a Semiring

Informal description

For any semiring $R$, there is at most one ring homomorphism from $\mathbb{Z}/n\mathbb{Z}$ to $R$.

ZMod.subsingleton_ringEquiv instance

[Semiring R] : Subsingleton (ZMod n ≃+* R)

Full source

instance subsingleton_ringEquiv [Semiring R] : Subsingleton (ZModZMod n ≃+* R) :=
  ⟨fun f g => by
    rw [RingEquiv.coe_ringHom_inj_iff]
    apply RingHom.ext_zmod _ _⟩

Uniqueness of Ring Isomorphisms from $\mathbb{Z}/n\mathbb{Z}$ to a Semiring

Informal description

For any semiring $R$, there is at most one ring isomorphism between $\mathbb{Z}/n\mathbb{Z}$ and $R$.

ZMod.ringHom_map_cast theorem

[NonAssocRing R] (f : R →+* ZMod n) (k : ZMod n) : f (cast k) = k

Full source

@[simp]
theorem ringHom_map_cast [NonAssocRing R] (f : R →+* ZMod n) (k : ZMod n) : f (cast k) = k := by
  cases n
  · dsimp [ZMod, ZMod.cast] at f k ⊢; simp
  · dsimp [ZMod.cast]
    rw [map_natCast, natCast_zmod_val]

Ring Homomorphism Preserves Canonical Map: $f(\mathrm{cast}(k)) = k$

Informal description

Let $R$ be a non-associative ring and let $f \colon R \to \mathbb{Z}/n\mathbb{Z}$ be a ring homomorphism. For any element $k \in \mathbb{Z}/n\mathbb{Z}$, the image of the canonical map $\mathrm{cast}(k) \in R$ under $f$ is equal to $k$, i.e., $f(\mathrm{cast}(k)) = k$.

ZMod.ringHom_rightInverse theorem

[NonAssocRing R] (f : R →+* ZMod n) : Function.RightInverse (cast : ZMod n → R) f

Full source

/-- Any ring homomorphism into `ZMod n` has a right inverse. -/
theorem ringHom_rightInverse [NonAssocRing R] (f : R →+* ZMod n) :
    Function.RightInverse (cast : ZMod n → R) f :=
  ringHom_map_cast f

Right Inverse Property of the Canonical Map for Ring Homomorphisms to $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any non-associative ring $R$ and any ring homomorphism $f \colon R \to \mathbb{Z}/n\mathbb{Z}$, the canonical map $\mathrm{cast} \colon \mathbb{Z}/n\mathbb{Z} \to R$ is a right inverse of $f$. That is, for every $k \in \mathbb{Z}/n\mathbb{Z}$, we have $f(\mathrm{cast}(k)) = k$.

ZMod.ringHom_surjective theorem

[NonAssocRing R] (f : R →+* ZMod n) : Function.Surjective f

Full source

/-- Any ring homomorphism into `ZMod n` is surjective. -/
theorem ringHom_surjective [NonAssocRing R] (f : R →+* ZMod n) : Function.Surjective f :=
  (ringHom_rightInverse f).surjective

Surjectivity of Ring Homomorphisms to $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any non-associative ring $R$ and any ring homomorphism $f \colon R \to \mathbb{Z}/n\mathbb{Z}$, the homomorphism $f$ is surjective.

ZMod.castHom_self theorem

: ZMod.castHom dvd_rfl (ZMod n) = RingHom.id (ZMod n)

Full source

@[simp]
lemma castHom_self : ZMod.castHom dvd_rfl (ZMod n) = RingHom.id (ZMod n) :=
  Subsingleton.elim _ _

Identity Property of the Canonical Homomorphism on $\mathbb{Z}/n\mathbb{Z}$

Informal description

The canonical ring homomorphism from $\mathbb{Z}/n\mathbb{Z}$ to itself, induced by the divisibility relation $n \mid n$, is equal to the identity ring homomorphism on $\mathbb{Z}/n\mathbb{Z}$.

ZMod.castHom_comp theorem

 {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
  (castHom hm (ZMod n)).comp (castHom hd (ZMod m)) = castHom (dvd_trans hm hd) (ZMod n)

Full source

@[simp]
lemma castHom_comp {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
    (castHom hm (ZMod n)).comp (castHom hd (ZMod m)) = castHom (dvd_trans hm hd) (ZMod n) :=
  RingHom.ext_zmod _ _

Composition of Canonical Homomorphisms for $\mathbb{Z}/n\mathbb{Z}$

Informal description

Let $n$, $m$, and $d$ be natural numbers such that $n$ divides $m$ and $m$ divides $d$. Then the composition of the canonical ring homomorphisms $\mathbb{Z}/d\mathbb{Z} \to \mathbb{Z}/m\mathbb{Z}$ and $\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ is equal to the canonical ring homomorphism $\mathbb{Z}/d\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ induced by the divisibility relation $n \mid d$.

ZMod.lift definition

: { f : ℤ →+ A // f n = 0 } ≃ (ZMod n →+ A)

Full source

/-- The map from `ZMod n` induced by `f : ℤ →+ A` that maps `n` to `0`. -/
def lift : { f : ℤ →+ A // f n = 0 }{ f : ℤ →+ A // f n = 0 } ≃ (ZMod n →+ A) :=
  (Equiv.subtypeEquivRight <| by
        intro f
        rw [ker_intCastAddHom]
        constructor
        · rintro hf _ ⟨x, rfl⟩
          simp only [f.map_zsmul, zsmul_zero, f.mem_ker, hf]
        · intro h
          exact h (AddSubgroup.mem_zmultiples _)).trans <|
    (Int.castAddHom (ZMod n)).liftOfRightInverse cast intCast_zmod_cast

Lifting of additive homomorphisms from integers to ZMod n

Informal description

The function `ZMod.lift` establishes an equivalence between: 1. The type of additive group homomorphisms $f \colon \mathbb{Z} \to A$ that satisfy $f(n) = 0$ 2. The type of additive group homomorphisms $\mathbb{Z}/n\mathbb{Z} \to A$ Given such an $f$, the corresponding homomorphism $\mathbb{Z}/n\mathbb{Z} \to A$ is obtained by lifting $f$ through the canonical projection $\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$.

ZMod.lift_coe theorem

(x : ℤ) : lift n f (x : ZMod n) = f.val x

Full source

@[simp]
theorem lift_coe (x : ℤ) : lift n f (x : ZMod n) = f.val x :=
  AddMonoidHom.liftOfRightInverse_comp_apply _ _ (fun _ => intCast_zmod_cast _) _ _

Commutativity of Lifting Diagram for $\mathbb{Z}/n\mathbb{Z}$ Homomorphisms

Informal description

For any integer $x \in \mathbb{Z}$ and any additive group homomorphism $f \colon \mathbb{Z} \to A$ satisfying $f(n) = 0$, the lift of $f$ to $\mathbb{Z}/n\mathbb{Z}$ evaluated at the image of $x$ in $\mathbb{Z}/n\mathbb{Z}$ equals $f(x)$. In other words, the following diagram commutes: \[ \begin{tikzcd} \mathbb{Z} \arrow[r, "f"] \arrow[d, "\text{mod }n"] & A \\ \mathbb{Z}/n\mathbb{Z} \arrow[ru, "\text{lift }f"] & \end{tikzcd} \] where the vertical map is the canonical projection modulo $n$.

ZMod.lift_castAddHom theorem

(x : ℤ) : lift n f (Int.castAddHom (ZMod n) x) = f.1 x

Full source

theorem lift_castAddHom (x : ℤ) : lift n f (Int.castAddHom (ZMod n) x) = f.1 x :=
  AddMonoidHom.liftOfRightInverse_comp_apply _ _ (fun _ => intCast_zmod_cast _) _ _

Lifting Property of Additive Homomorphisms from $\mathbb{Z}$ to $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any integer $x \in \mathbb{Z}$, the lift of an additive group homomorphism $f \colon \mathbb{Z} \to A$ (satisfying $f(n) = 0$) evaluated at the image of $x$ under the canonical additive homomorphism $\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ equals $f(x)$. In symbols: \[ \text{lift}_n(f)(\text{Int.castAddHom}(\mathbb{Z}/n\mathbb{Z})(x)) = f(x). \]

ZMod.lift_comp_coe theorem

: ZMod.lift n f ∘ ((↑) : ℤ → _) = f

Full source

@[simp]
theorem lift_comp_coe : ZMod.liftZMod.lift n f ∘ ((↑) : ℤ → _) = f :=
  funext <| lift_coe _ _

Commutativity of Lifting Diagram for $\mathbb{Z}/n\mathbb{Z}$ Homomorphisms via Composition

Informal description

For any additive group homomorphism $f \colon \mathbb{Z} \to A$ satisfying $f(n) = 0$, the composition of the lift of $f$ to $\mathbb{Z}/n\mathbb{Z}$ with the canonical projection $\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ equals $f$ itself. In other words, the following diagram commutes: \[ \begin{tikzcd} \mathbb{Z} \arrow[r, "f"] \arrow[d, "\text{mod }n"] & A \\ \mathbb{Z}/n\mathbb{Z} \arrow[ru, "\text{lift }f"] & \end{tikzcd} \] where the vertical map is the canonical projection modulo $n$.

ZMod.lift_comp_castAddHom theorem

: (ZMod.lift n f).comp (Int.castAddHom (ZMod n)) = f

Full source

@[simp]
theorem lift_comp_castAddHom : (ZMod.lift n f).comp (Int.castAddHom (ZMod n)) = f :=
  AddMonoidHom.ext <| lift_castAddHom _ _

Composition of Lifted Homomorphism with Canonical Projection Equals Original Homomorphism

Informal description

For any additive group homomorphism $f \colon \mathbb{Z} \to A$ satisfying $f(n) = 0$, the composition of the lifted homomorphism $\mathbb{Z}/n\mathbb{Z} \to A$ with the canonical homomorphism $\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ equals $f$. In symbols: \[ \text{lift}_n(f) \circ \text{Int.castAddHom}(\mathbb{Z}/n\mathbb{Z}) = f. \]

ZMod.lift_injective theorem

{f : { f : ℤ →+ A // f n = 0 }} : Injective (lift n f) ↔ ∀ m, f.1 m = 0 → (m : ZMod n) = 0

Full source

lemma lift_injective {f : {f : ℤ →+ A // f n = 0}} :
    InjectiveInjective (lift n f) ↔ ∀ m, f.1 m = 0 → (m : ZMod n) = 0 := by
  simp only [← AddMonoidHom.ker_eq_bot_iff, eq_bot_iff, SetLike.le_def,
    ZMod.intCast_surjective.forall, ZMod.lift_coe, AddMonoidHom.mem_ker, AddSubgroup.mem_bot]

Injectivity Criterion for Lifted Homomorphisms from $\mathbb{Z}/n\mathbb{Z}$ to an Additive Group

Informal description

Let $A$ be an additive group and $f \colon \mathbb{Z} \to A$ be an additive group homomorphism such that $f(n) = 0$. The lifted homomorphism $\text{lift}_n f \colon \mathbb{Z}/n\mathbb{Z} \to A$ is injective if and only if for every integer $m$, if $f(m) = 0$ then $m \equiv 0 \pmod{n}$ in $\mathbb{Z}/n\mathbb{Z}$.

zmod_smul_mem theorem

(hx : x ∈ K) : ∀ a : ZMod n, a • x ∈ K

Full source

lemma zmod_smul_mem (hx : x ∈ K) : ∀ a : ZMod n, a • x ∈ K := by
  simpa [ZMod.forall, Int.cast_smul_eq_zsmul] using zsmul_mem hx

Closure under $\mathbb{Z}/n\mathbb{Z}$-scalar multiplication in additive subgroups

Informal description

Let $K$ be a subset of an additive commutative group $G$ that is closed under scalar multiplication by elements of $\mathbb{Z}/n\mathbb{Z}$. If $x \in K$, then for any $a \in \mathbb{Z}/n\mathbb{Z}$, the scalar multiple $a \cdot x$ is also in $K$.

smulMemClass theorem

: SMulMemClass S (ZMod n) G

Full source

/-- 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`. -/
lemma smulMemClass : SMulMemClass S (ZMod n) G where smul_mem _ _ {_x} hx := zmod_smul_mem hx _

Closure of Set-like Structures under $\mathbb{Z}/n\mathbb{Z}$-scalar Multiplication in Additive Commutative Groups

Informal description

Let $G$ be an additive commutative group and $S$ a set-like structure on $G$ that is closed under scalar multiplication by elements of $\mathbb{Z}/n\mathbb{Z}$. Then $S$ forms a scalar multiplication memory class for the action of $\mathbb{Z}/n\mathbb{Z}$ on $G$.

AddSubgroupClass.instZModSMul instance

: SMul (ZMod n) K

Full source

instance instZModSMul : SMul (ZMod n) K where smul a x := ⟨a • x, zmod_smul_mem x.2 _⟩

Scalar Multiplication by $\mathbb{Z}/n\mathbb{Z}$ on Additive Subgroups

Informal description

For any additive subgroup $K$ of an additive commutative group $G$, there is a canonical scalar multiplication operation of $\mathbb{Z}/n\mathbb{Z}$ on $K$, making $K$ a module over $\mathbb{Z}/n\mathbb{Z}$.

AddSubgroupClass.coe_zmod_smul theorem

(a : ZMod n) (x : K) : ↑(a • x) = (a • x : G)

Full source

@[simp, norm_cast] lemma coe_zmod_smul (a : ZMod n) (x : K) : ↑(a • x) = (a • x : G) := rfl

Preservation of $\mathbb{Z}/n\mathbb{Z}$-scalar multiplication under subgroup inclusion

Informal description

Let $K$ be an additive subgroup of an additive commutative group $G$, and let $n$ be a natural number. For any element $a \in \mathbb{Z}/n\mathbb{Z}$ and any element $x \in K$, the scalar multiplication $a \cdot x$ in $K$ coincides with the scalar multiplication $a \cdot x$ in $G$ under the canonical inclusion map from $K$ to $G$. In other words, the inclusion map preserves the $\mathbb{Z}/n\mathbb{Z}$-scalar multiplication.

AddSubgroupClass.instZModModule instance

: Module (ZMod n) K

Full source

instance instZModModule : Module (ZMod n) K :=
  Subtype.coe_injective.module _ (AddSubmonoidClass.subtype K) coe_zmod_smul

$\mathbb{Z}/n\mathbb{Z}$-Module Structure on Additive Subgroups

Informal description

For any additive subgroup $K$ of an additive commutative group $G$, there is a canonical module structure over $\mathbb{Z}/n\mathbb{Z}$ on $K$, where scalar multiplication is defined by the natural action of $\mathbb{Z}/n\mathbb{Z}$ on $G$.

ZModModule.char_nsmul_eq_zero theorem

(x : G) : n • x = 0

Full source

lemma ZModModule.char_nsmul_eq_zero (x : G) : n • x = 0 := by
  simp [← Nat.cast_smul_eq_nsmul (ZMod n)]

$n$-torsion property in $\mathbb{Z}/n\mathbb{Z}$-modules

Informal description

For any element $x$ in an additive commutative group $G$ equipped with a $\mathbb{Z}/n\mathbb{Z}$-module structure, the scalar multiplication $n \cdot x$ equals the zero element of $G$.

ZModModule.char_ne_one theorem

[Nontrivial G] : n ≠ 1

Full source

lemma ZModModule.char_ne_one [Nontrivial G] : n ≠ 1 := by
  rintro rfl
  obtain ⟨x, hx⟩ := exists_ne (0 : G)
  exact hx <| by simpa using char_nsmul_eq_zero 1 x

Non-trivial $\mathbb{Z}/n\mathbb{Z}$-modules have $n \neq 1$

Informal description

For any nontrivial additive commutative group $G$ equipped with a $\mathbb{Z}/n\mathbb{Z}$-module structure, the modulus $n$ is not equal to $1$.

ZModModule.two_le_char theorem

[NeZero n] [Nontrivial G] : 2 ≤ n

Full source

lemma ZModModule.two_le_char [NeZero n] [Nontrivial G] : 2 ≤ n := by
  have := NeZero.ne n
  have := char_ne_one n G
  omega

Lower Bound on Characteristic in Nontrivial $\mathbb{Z}/n\mathbb{Z}$-Modules

Informal description

For any nontrivial additive commutative group $G$ equipped with a $\mathbb{Z}/n\mathbb{Z}$-module structure where $n$ is a nonzero natural number, the modulus $n$ satisfies $n \geq 2$.

ZModModule.periodicPts_add_left theorem

[NeZero n] (x : G) : periodicPts (x + ·) = .univ

Full source

lemma ZModModule.periodicPts_add_left [NeZero n] (x : G) : periodicPts (x + ·) = .univ :=
  Set.eq_univ_of_forall fun y ↦ ⟨n, NeZero.pos n, by
    simpa [char_nsmul_eq_zero, IsPeriodicPt] using isFixedPt_id _⟩

Periodic Points of Left Translation in $\mathbb{Z}/n\mathbb{Z}$-Modules Cover the Entire Group

Informal description

Let $G$ be an additive commutative group with a $\mathbb{Z}/n\mathbb{Z}$-module structure, where $n$ is a nonzero natural number. For any element $x \in G$, the set of periodic points of the left translation function $y \mapsto x + y$ is the entire group $G$, i.e., $\{ y \in G \mid \exists k > 0, (x + \cdot)^k(y) = y \} = G$.

ZModModule.add_self theorem

(x : G) : x + x = 0

Full source

lemma ZModModule.add_self (x : G) : x + x = 0 := by
  simpa [two_nsmul] using char_nsmul_eq_zero 2 x

Self-Addition Vanishes in $\mathbb{Z}/n\mathbb{Z}$-Modules

Informal description

For any element $x$ in an additive commutative group $G$ equipped with a $\mathbb{Z}/n\mathbb{Z}$-module structure, the sum of $x$ with itself equals the zero element, i.e., $x + x = 0$.

ZModModule.neg_eq_self theorem

(x : G) : -x = x

Full source

lemma ZModModule.neg_eq_self (x : G) : -x = x := by simp [add_self, eq_comm, ← sub_eq_zero]

Negation Equals Identity in $\mathbb{Z}/n\mathbb{Z}$-Modules

Informal description

For any element $x$ in an additive commutative group $G$ equipped with a $\mathbb{Z}/n\mathbb{Z}$-module structure, the negation of $x$ is equal to $x$ itself, i.e., $-x = x$.

ZModModule.sub_eq_add theorem

(x y : G) : x - y = x + y

Full source

lemma ZModModule.sub_eq_add (x y : G) : x - y = x + y := by simp [neg_eq_self, sub_eq_add_neg]

Subtraction Equals Addition in $\mathbb{Z}/n\mathbb{Z}$-Modules

Informal description

For any elements $x$ and $y$ in an additive commutative group $G$ equipped with a $\mathbb{Z}/n\mathbb{Z}$-module structure, the difference $x - y$ equals the sum $x + y$.

ZModModule.add_add_add_cancel theorem

(x y z : G) : (x + y) + (y + z) = x + z

Full source

lemma ZModModule.add_add_add_cancel (x y z : G) : (x + y) + (y + z) = x + z := by
  simpa [sub_eq_add] using sub_add_sub_cancel x y z

Cancellation Identity in $\mathbb{Z}/n\mathbb{Z}$-Modules: $(x + y) + (y + z) = x + z$

Informal description

For any elements $x, y, z$ in an additive commutative group $G$ equipped with a $\mathbb{Z}/n\mathbb{Z}$-module structure, the following identity holds: $(x + y) + (y + z) = x + z$.

nsmul_zmod_val_inv_nsmul theorem

(hn : (Nat.card α).Coprime n) (a : α) : n • (n⁻¹ : ZMod (Nat.card α)).val • a = a

Full source

@[simp]
lemma nsmul_zmod_val_inv_nsmul (hn : (Nat.card α).Coprime n) (a : α) :
    n • (n⁻¹ : ZMod (Nat.card α)).val • a = a := by
  rw [← mul_nsmul', ← mod_natCard_nsmul, ← ZMod.val_natCast, Nat.cast_mul,
    ZMod.mul_val_inv hn.symm, ZMod.val_one_eq_one_mod, mod_natCard_nsmul, one_nsmul]

Additive Scalar Multiplication by Coprime Inverse: $n \cdot (n^{-1} \cdot a) = a$

Informal description

Let $\alpha$ be a type with finite cardinality, and let $n$ be a natural number coprime to $\text{card}(\alpha)$. Then for any element $a \in \alpha$, the following equality holds in the additive group of $\alpha$: \[ n \cdot \left( (n^{-1} \bmod \text{card}(\alpha)) \cdot a \right) = a, \] where $n^{-1}$ denotes the multiplicative inverse of $n$ modulo $\text{card}(\alpha)$, and $\cdot$ denotes scalar multiplication.

zmod_val_inv_nsmul_nsmul theorem

(hn : (Nat.card α).Coprime n) (a : α) : (n⁻¹ : ZMod (Nat.card α)).val • n • a = a

Full source

@[simp]
lemma zmod_val_inv_nsmul_nsmul (hn : (Nat.card α).Coprime n) (a : α) :
    (n⁻¹ : ZMod (Nat.card α)).val • n • a = a := by
  rw [nsmul_left_comm, nsmul_zmod_val_inv_nsmul hn]

Additive Scalar Multiplication by Coprime Inverse: $(n^{-1} \bmod |G|) \cdot (n \cdot a) = a$

Informal description

Let $\alpha$ be a type with finite cardinality, and let $n$ be a natural number coprime to $\mathrm{card}(\alpha)$. Then for any element $a \in \alpha$, the following equality holds in the additive group of $\alpha$: \[ (n^{-1} \bmod \mathrm{card}(\alpha)) \cdot (n \cdot a) = a, \] where $n^{-1}$ denotes the multiplicative inverse of $n$ modulo $\mathrm{card}(\alpha)$, and $\cdot$ denotes scalar multiplication.

pow_zmod_val_inv_pow theorem

(hn : (Nat.card α).Coprime n) (a : α) : (a ^ (n⁻¹ : ZMod (Nat.card α)).val) ^ n = a

Full source

@[to_additive existing (attr := simp) nsmul_zmod_val_inv_nsmul]
lemma pow_zmod_val_inv_pow (hn : (Nat.card α).Coprime n) (a : α) :
    (a ^ (n⁻¹ : ZMod (Nat.card α)).val) ^ n = a := by
  rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]

Power Identity for Coprime Exponents: $\left(a^{(n^{-1} \bmod |G|)}\right)^n = a$

Informal description

Let $\alpha$ be a type with a group structure, and let $n$ be a natural number such that $n$ is coprime with the cardinality of $\alpha$ (denoted $\mathrm{card}(\alpha)$). Then for any element $a \in \alpha$, we have \[ \left(a^{(n^{-1} \bmod \mathrm{card}(\alpha))}\right)^n = a, \] where $n^{-1} \bmod \mathrm{card}(\alpha)$ denotes the multiplicative inverse of $n$ modulo $\mathrm{card}(\alpha)$.

pow_pow_zmod_val_inv theorem

(hn : (Nat.card α).Coprime n) (a : α) : (a ^ n) ^ (n⁻¹ : ZMod (Nat.card α)).val = a

Full source

@[to_additive existing (attr := simp) zmod_val_inv_nsmul_nsmul]
lemma pow_pow_zmod_val_inv (hn : (Nat.card α).Coprime n) (a : α) :
    (a ^ n) ^ (n⁻¹ : ZMod (Nat.card α)).val = a := by rw [pow_right_comm, pow_zmod_val_inv_pow hn]

Inverse Power Identity for Coprime Exponents: $(a^n)^{(n^{-1} \bmod |G|)} = a$

Informal description

Let $\alpha$ be a type with a group structure, and let $n$ be a natural number such that $n$ is coprime with the cardinality of $\alpha$ (denoted $\mathrm{card}(\alpha)$). Then for any element $a \in \alpha$, we have \[ (a^n)^{(n^{-1} \bmod \mathrm{card}(\alpha))} = a, \] where $n^{-1} \bmod \mathrm{card}(\alpha)$ denotes the multiplicative inverse of $n$ modulo $\mathrm{card}(\alpha)$.

Nat.range_mul_add theorem

(m k : ℕ) : Set.range (fun n : ℕ ↦ m * n + k) = {n : ℕ | (n : ZMod m) = k ∧ k ≤ n}

Full source

/-- The range of `(m * · + k)` on natural numbers is the set of elements `≥ k` in the
residue class of `k` mod `m`. -/
lemma Nat.range_mul_add (m k : ℕ) :
    Set.range (fun n : ℕ ↦ m * n + k) = {n : ℕ | (n : ZMod m) = k ∧ k ≤ n} := by
  ext n
  simp only [Set.mem_range, Set.mem_setOf_eq]
  conv => enter [1, 1, y]; rw [add_comm, eq_comm]
  refine ⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
  · simpa using congr_arg ((↑) : ℕ → ZMod m) ha
  · obtain ⟨a, ha⟩ := le_iff_exists_add.mp H₂
    simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_zmod_eq_zero_iff_dvd] at H₁
    obtain ⟨b, rfl⟩ := H₁
    exact ⟨b, ha⟩

Range of Linear Function in Natural Numbers Modulo $m$

Informal description

For any natural numbers $m$ and $k$, the range of the function $n \mapsto m \cdot n + k$ on natural numbers is equal to the set of natural numbers $n$ such that $n \equiv k \pmod{m}$ and $k \leq n$.

Nat.residueClassesEquiv definition

(N : ℕ) [NeZero N] : ℕ ≃ ZMod N × ℕ

Full source

/-- Equivalence between `ℕ` and `ZMod N × ℕ`, sending `n` to `(n mod N, n / N)`. -/
def Nat.residueClassesEquiv (N : ℕ) [NeZero N] : ℕℕ ≃ ZMod N × ℕ where
  toFun n := (↑n, n / N)
  invFun p := p.1.val + N * p.2
  left_inv n := by simpa only [val_natCast] using mod_add_div n N
  right_inv p := by
    ext1
    · simp only [add_comm p.1.val, cast_add, cast_mul, natCast_self, zero_mul, natCast_val,
        cast_id', id_eq, zero_add]
    · simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
        (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]

Natural numbers as residue classes and quotients

Informal description

For any positive natural number $N$, there is a bijection between the natural numbers $\mathbb{N}$ and the product type $\mathbb{Z}/N\mathbb{Z} \times \mathbb{N}$. The bijection is given by: - The forward map sends $n \in \mathbb{N}$ to $(n \mod N, n / N)$ - The inverse map sends $(a, k) \in \mathbb{Z}/N\mathbb{Z} \times \mathbb{N}$ to $\text{val}(a) + N \cdot k$ This equivalence satisfies: 1. Left inverse property: composing the forward and inverse maps returns the original natural number 2. Right inverse property: composing the inverse and forward maps returns the original pair

Definitions