import algebra.char_p.basic

import data.fintype.units

import data.nat.parity

import tactic.fin_cases

open function

namespace zmod

instance : char_zero (zmod 0) := (by apply_instance : char_zero ℤ)

def val : Π {n : ℕ}, zmod n → ℕ

| 0 := int.nat_abs

| (n+1) := (coe : fin (n + 1) → ℕ)

lemma val_lt {n : ℕ} [ne_zero n] (a : zmod n) : a.val < n :=

casesI n,

{ cases ne_zero.ne 0 rfl },

exact fin.is_lt a

lemma val_le {n : ℕ} [ne_zero n] (a : zmod n) : a.val ≤ n :=

a.val_lt.le

@[simp] lemma val_zero : ∀ {n}, (0 : zmod n).val = 0

| 0 := rfl

| (n+1) := rfl

@[simp] lemma val_one' : (1 : zmod 0).val = 1 := rfl

@[simp] lemma val_neg' {n : zmod 0} : (-n).val = n.val := by simp [val]

@[simp] lemma val_mul' {m n : zmod 0} : (m * n).val = m.val * n.val :=

by simp [val, int.nat_abs_mul]

lemma val_nat_cast {n : ℕ} (a : ℕ) : (a : zmod n).val = a % n :=

casesI n,

{ rw [nat.mod_zero],

exact int.nat_abs_of_nat a, },

rw ← fin.of_nat_eq_coe,

refl

instance (n : ℕ) : char_p (zmod n) n :=

{ cast_eq_zero_iff :=

begin

intro k,

cases n,

{ simp only [zero_dvd_iff, int.coe_nat_eq_zero], },

rw [fin.eq_iff_veq],

show (k : zmod (n+1)).val = (0 : zmod (n+1)).val ↔ _,

rw [val_nat_cast, val_zero, nat.dvd_iff_mod_eq_zero],

end }

@[simp] lemma add_order_of_one (n : ℕ) : add_order_of (1 : zmod n) = n :=

char_p.eq _ (char_p.add_order_of_one _) (zmod.char_p n)

@[simp] lemma add_order_of_coe (a : ℕ) {n : ℕ} (n0 : n ≠ 0) :

add_order_of (a : zmod n) = n / n.gcd a :=

cases a,

simp [nat.pos_of_ne_zero n0],

rw [← nat.smul_one_eq_coe, add_order_of_nsmul' _ a.succ_ne_zero, zmod.add_order_of_one],

@[simp] lemma add_order_of_coe' {a : ℕ} (n : ℕ) (a0 : a ≠ 0) :

add_order_of (a : zmod n) = n / n.gcd a :=

by rw [← nat.smul_one_eq_coe, add_order_of_nsmul' _ a0, zmod.add_order_of_one]

lemma ring_char_zmod_n (n : ℕ) : ring_char (zmod n) = n :=

by { rw ring_char.eq_iff, exact zmod.char_p n, }

@[simp] lemma nat_cast_self (n : ℕ) : (n : zmod n) = 0 :=

char_p.cast_eq_zero (zmod n) n

@[simp] lemma nat_cast_self' (n : ℕ) : (n + 1 : zmod (n + 1)) = 0 :=

by rw [← nat.cast_add_one, nat_cast_self (n + 1)]

section universal_property

variables {n : ℕ} {R : Type*}

variables [add_group_with_one R]

def cast : Π {n : ℕ}, zmod n → R

| 0 := int.cast

| (n+1) := λ i, i.val

@[priority 900] instance (n : ℕ) : has_coe_t (zmod n) R := ⟨cast⟩

@[simp] lemma cast_zero : ((0 : zmod n) : R) = 0 :=

by cases n; simp

lemma cast_eq_val [ne_zero n] (a : zmod n) : (a : R) = a.val :=

casesI n,

{ cases ne_zero.ne 0 rfl },

refl,

variables {S : Type*} [add_group_with_one S]

@[simp] lemma _root_.prod.fst_zmod_cast (a : zmod n) : (a : R × S).fst = a :=

by cases n; simp

@[simp] lemma _root_.prod.snd_zmod_cast (a : zmod n) : (a : R × S).snd = a :=

by cases n; simp

lemma nat_cast_zmod_val {n : ℕ} [ne_zero n] (a : zmod n) : (a.val : zmod n) = a :=

casesI n,

{ cases ne_zero.ne 0 rfl },

{ apply fin.coe_coe_eq_self }

lemma nat_cast_right_inverse [ne_zero n] : function.right_inverse val (coe : ℕ → zmod n) :=

nat_cast_zmod_val

lemma nat_cast_zmod_surjective [ne_zero n] : function.surjective (coe : ℕ → zmod n) :=

nat_cast_right_inverse.surjective

@[norm_cast] lemma int_cast_zmod_cast (a : zmod n) : ((a : ℤ) : zmod n) = a :=

cases n,

{ rw [int.cast_id a, int.cast_id a], },

{ rw [coe_coe, int.cast_coe_nat, fin.coe_coe_eq_self] }

lemma int_cast_right_inverse : function.right_inverse (coe : zmod n → ℤ) (coe : ℤ → zmod n) :=

int_cast_zmod_cast

lemma int_cast_surjective : function.surjective (coe : ℤ → zmod n) :=

int_cast_right_inverse.surjective

lemma cast_id : ∀ n (i : zmod n), ↑i = i

| 0 i := int.cast_id i

| (n+1) i := nat_cast_zmod_val i

lemma cast_id' : (coe : zmod n → zmod n) = id := funext (cast_id n)

variables (R) [ring R]

@[simp] lemma nat_cast_comp_val [ne_zero n] :

(coe : ℕ → R) ∘ (val : zmod n → ℕ) = coe :=

casesI n,

{ cases ne_zero.ne 0 rfl },

refl

@[simp] lemma int_cast_comp_cast : (coe : ℤ → R) ∘ (coe : zmod n → ℤ) = coe :=

cases n,

{ exact congr_arg ((∘) int.cast) zmod.cast_id', },

{ ext, simp }

variables {R}

@[simp] lemma nat_cast_val [ne_zero n] (i : zmod n) : (i.val : R) = i :=

congr_fun (nat_cast_comp_val R) i

@[simp] lemma int_cast_cast (i : zmod n) : ((i : ℤ) : R) = i :=

congr_fun (int_cast_comp_cast R) i

lemma coe_add_eq_ite {n : ℕ} (a b : zmod n) :

(↑(a + b) : ℤ) = if (n : ℤ) ≤ a + b then a + b - n else a + b :=

cases n,

{ simp },

simp only [coe_coe, fin.coe_add_eq_ite,

← int.coe_nat_add, ← int.coe_nat_succ, int.coe_nat_le],

split_ifs with h,

{ exact int.coe_nat_sub h },

{ refl }

section char_dvd

variables {n} {m : ℕ} [char_p R m]

@[simp] lemma cast_one (h : m ∣ n) : ((1 : zmod n) : R) = 1 :=

casesI n,

{ exact int.cast_one },

show ((1 % (n+1) : ℕ) : R) = 1,

cases n, { rw [nat.dvd_one] at h, substI m, apply subsingleton.elim },

rw nat.mod_eq_of_lt,

{ exact nat.cast_one },

exact nat.lt_of_sub_eq_succ rfl

lemma cast_add (h : m ∣ n) (a b : zmod n) : ((a + b : zmod n) : R) = a + b :=

casesI n,

{ apply int.cast_add },

simp only [coe_coe],

symmetry,

erw [fin.coe_add, ← nat.cast_add, ← sub_eq_zero, ← nat.cast_sub (nat.mod_le _ _),

@char_p.cast_eq_zero_iff R _ m],

exact h.trans (nat.dvd_sub_mod _),

lemma cast_mul (h : m ∣ n) (a b : zmod n) : ((a * b : zmod n) : R) = a * b :=

casesI n,

{ apply int.cast_mul },

simp only [coe_coe],

symmetry,

erw [fin.coe_mul, ← nat.cast_mul, ← sub_eq_zero, ← nat.cast_sub (nat.mod_le _ _),

@char_p.cast_eq_zero_iff R _ m],

exact h.trans (nat.dvd_sub_mod _),

def cast_hom (h : m ∣ n) (R : Type*) [ring R] [char_p R m] : zmod n →+* R :=

{ to_fun := coe,

map_zero' := cast_zero,

map_one' := cast_one h,

map_add' := cast_add h,

map_mul' := cast_mul h }

@[simp] lemma cast_hom_apply {h : m ∣ n} (i : zmod n) : cast_hom h R i = i := rfl

lemma cast_sub (h : m ∣ n) (a b : zmod n) : ((a - b : zmod n) : R) = a - b :=

(cast_hom h R).map_sub a b

lemma cast_neg (h : m ∣ n) (a : zmod n) : ((-a : zmod n) : R) = -a :=

(cast_hom h R).map_neg a

lemma cast_pow (h : m ∣ n) (a : zmod n) (k : ℕ) : ((a ^ k : zmod n) : R) = a ^ k :=

(cast_hom h R).map_pow a k

lemma cast_nat_cast (h : m ∣ n) (k : ℕ) : ((k : zmod n) : R) = k :=

map_nat_cast (cast_hom h R) k

lemma cast_int_cast (h : m ∣ n) (k : ℤ) : ((k : zmod n) : R) = k := map_int_cast (cast_hom h R) k

end char_dvd

section char_eq

variable [char_p R n]

@[simp] lemma cast_one' : ((1 : zmod n) : R) = 1 :=

cast_one dvd_rfl

@[simp] lemma cast_add' (a b : zmod n) : ((a + b : zmod n) : R) = a + b :=

cast_add dvd_rfl a b

@[simp] lemma cast_mul' (a b : zmod n) : ((a * b : zmod n) : R) = a * b :=

cast_mul dvd_rfl a b

@[simp] lemma cast_sub' (a b : zmod n) : ((a - b : zmod n) : R) = a - b :=

cast_sub dvd_rfl a b

@[simp] lemma cast_pow' (a : zmod n) (k : ℕ) : ((a ^ k : zmod n) : R) = a ^ k :=

cast_pow dvd_rfl a k

lemma cast_nat_cast' (k : ℕ) : ((k : zmod n) : R) = k :=

cast_nat_cast dvd_rfl k

lemma cast_int_cast' (k : ℤ) : ((k : zmod n) : R) = k :=

cast_int_cast dvd_rfl k

variables (R)

lemma cast_hom_injective : function.injective (zmod.cast_hom (dvd_refl n) R) :=

rw injective_iff_map_eq_zero,

intro x,

obtain ⟨k, rfl⟩ := zmod.int_cast_surjective x,

rw [map_int_cast, char_p.int_cast_eq_zero_iff R n,

char_p.int_cast_eq_zero_iff (zmod n) n],

exact id

lemma cast_hom_bijective [fintype R] (h : fintype.card R = n) :

function.bijective (zmod.cast_hom (dvd_refl n) R) :=

haveI : ne_zero n :=

⟨begin

intro hn,

rw hn at h,

exact (fintype.card_eq_zero_iff.mp h).elim' 0

end⟩,

rw [fintype.bijective_iff_injective_and_card, zmod.card, h, eq_self_iff_true, and_true],

apply zmod.cast_hom_injective

noncomputable def ring_equiv [fintype R] (h : fintype.card R = n) : zmod n ≃+* R :=

ring_equiv.of_bijective _ (zmod.cast_hom_bijective R h)

def ring_equiv_congr {m n : ℕ} (h : m = n) : zmod m ≃+* zmod n :=

cases m; cases n,

{ exact ring_equiv.refl _ },

{ exfalso, exact n.succ_ne_zero h.symm },

{ exfalso, exact m.succ_ne_zero h },

{ exact

{ map_mul' := λ a b, begin

rw [order_iso.to_fun_eq_coe], ext,

rw [fin.coe_cast, fin.coe_mul, fin.coe_mul, fin.coe_cast, fin.coe_cast, ← h] end,

map_add' := λ a b, begin

rw [order_iso.to_fun_eq_coe], ext,

rw [fin.coe_cast, fin.coe_add, fin.coe_add, fin.coe_cast, fin.coe_cast, ← h] end,

..fin.cast h } }

end char_eq

end universal_property

lemma int_coe_eq_int_coe_iff (a b : ℤ) (c : ℕ) :

(a : zmod c) = (b : zmod c) ↔ a ≡ b [ZMOD c] :=

char_p.int_cast_eq_int_cast (zmod c) c

lemma int_coe_eq_int_coe_iff' (a b : ℤ) (c : ℕ) :

(a : zmod c) = (b : zmod c) ↔ a % c = b % c :=

zmod.int_coe_eq_int_coe_iff a b c

lemma nat_coe_eq_nat_coe_iff (a b c : ℕ) :

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

by simpa [int.coe_nat_modeq_iff] using zmod.int_coe_eq_int_coe_iff a b c

lemma nat_coe_eq_nat_coe_iff' (a b c : ℕ) :

(a : zmod c) = (b : zmod c) ↔ a % c = b % c :=

zmod.nat_coe_eq_nat_coe_iff a b c

lemma int_coe_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) : (a : zmod b) = 0 ↔ (b : ℤ) ∣ a :=

by rw [← int.cast_zero, zmod.int_coe_eq_int_coe_iff, int.modeq_zero_iff_dvd]

lemma int_coe_eq_int_coe_iff_dvd_sub (a b : ℤ) (c : ℕ) : (a : zmod c) = ↑b ↔ ↑c ∣ b-a :=

rw [zmod.int_coe_eq_int_coe_iff, int.modeq_iff_dvd],

lemma nat_coe_zmod_eq_zero_iff_dvd (a b : ℕ) : (a : zmod b) = 0 ↔ b ∣ a :=

by rw [← nat.cast_zero, zmod.nat_coe_eq_nat_coe_iff, nat.modeq_zero_iff_dvd]

lemma val_int_cast {n : ℕ} (a : ℤ) [ne_zero n] : ↑(a : zmod n).val = a % n :=

have hle : (0 : ℤ) ≤ ↑(a : zmod n).val := int.coe_nat_nonneg _,

have hlt : ↑(a : zmod n).val < (n : ℤ) := int.coe_nat_lt.mpr (zmod.val_lt a),

refine (int.mod_eq_of_lt hle hlt).symm.trans _,

rw [←zmod.int_coe_eq_int_coe_iff', int.cast_coe_nat, zmod.nat_cast_val, zmod.cast_id],

lemma coe_int_cast {n : ℕ} (a : ℤ) : ↑(a : zmod n) = a % n :=

cases n,

{ rw [int.coe_nat_zero, int.mod_zero, int.cast_id, int.cast_id] },

{ rw [←val_int_cast, val, coe_coe] },

@[simp] lemma val_neg_one (n : ℕ) : (-1 : zmod n.succ).val = n :=

rw [val, fin.coe_neg],

cases n,

{ rw [nat.mod_one] },

{ rw [fin.coe_one, nat.succ_add_sub_one, nat.mod_eq_of_lt (nat.lt.base _)] },

lemma cast_neg_one {R : Type*} [ring R] (n : ℕ) : ↑(-1 : zmod n) = (n - 1 : R) :=

cases n,

{ rw [int.cast_neg, int.cast_one, nat.cast_zero, zero_sub] },

{ rw [←nat_cast_val, val_neg_one, nat.cast_succ, add_sub_cancel] },

lemma cast_sub_one {R : Type*} [ring R] {n : ℕ} (k : zmod n) :

((k - 1 : zmod n) : R) = (if k = 0 then n else k) - 1 :=

split_ifs with hk,

{ rw [hk, zero_sub, zmod.cast_neg_one] },

{ cases n,

{ rw [int.cast_sub, int.cast_one] },

{ rw [←zmod.nat_cast_val, zmod.val, fin.coe_sub_one, if_neg],

{ rw [nat.cast_sub, nat.cast_one, coe_coe],

rwa [fin.ext_iff, fin.coe_zero, ←ne, ←nat.one_le_iff_ne_zero] at hk },

{ exact hk } } },

lemma nat_coe_zmod_eq_iff (p : ℕ) (n : ℕ) (z : zmod p) [ne_zero p] :

↑n = z ↔ ∃ k, n = z.val + p * k :=

split,

{ rintro rfl,

refine ⟨n / p, _⟩,

rw [val_nat_cast, nat.mod_add_div] },

{ rintro ⟨k, rfl⟩,

rw [nat.cast_add, nat_cast_zmod_val, nat.cast_mul, nat_cast_self, zero_mul, add_zero] }

lemma int_coe_zmod_eq_iff (p : ℕ) (n : ℤ) (z : zmod p) [ne_zero p] :

↑n = z ↔ ∃ k, n = z.val + p * k :=

split,

{ rintro rfl,

refine ⟨n / p, _⟩,

rw [val_int_cast, int.mod_add_div] },

{ rintro ⟨k, rfl⟩,

rw [int.cast_add, int.cast_mul, int.cast_coe_nat, int.cast_coe_nat, nat_cast_val,

zmod.nat_cast_self, zero_mul, add_zero, cast_id] }

lemma int_cast_mod (a : ℤ) (b : ℕ) : ((a % b : ℤ) : zmod b) = (a : zmod b) :=

rw zmod.int_coe_eq_int_coe_iff,

apply int.mod_modeq,

lemma ker_int_cast_add_hom (n : ℕ) :

(int.cast_add_hom (zmod n)).ker = add_subgroup.zmultiples n :=

by { ext, rw [int.mem_zmultiples_iff, add_monoid_hom.mem_ker,

int.coe_cast_add_hom, int_coe_zmod_eq_zero_iff_dvd] }

lemma ker_int_cast_ring_hom (n : ℕ) :

(int.cast_ring_hom (zmod n)).ker = ideal.span ({n} : set ℤ) :=

by { ext, rw [ideal.mem_span_singleton, ring_hom.mem_ker,

int.coe_cast_ring_hom, int_coe_zmod_eq_zero_iff_dvd] }

local attribute [semireducible] int.nonneg

@[simp] lemma nat_cast_to_nat (p : ℕ) :

∀ {z : ℤ} (h : 0 ≤ z), (z.to_nat : zmod p) = z

| (n : ℕ) h := by simp only [int.cast_coe_nat, int.to_nat_coe_nat]

| -[1+n] h := false.elim h

lemma val_injective (n : ℕ) [ne_zero n] :

function.injective (zmod.val : zmod n → ℕ) :=

casesI n,

{ cases ne_zero.ne 0 rfl },

assume a b h,

ext,

exact h

lemma val_one_eq_one_mod (n : ℕ) : (1 : zmod n).val = 1 % n :=

by rw [← nat.cast_one, val_nat_cast]

lemma 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 _) }

lemma val_add {n : ℕ} [ne_zero n] (a b : zmod n) : (a + b).val = (a.val + b.val) % n :=

casesI n,

{ cases ne_zero.ne 0 rfl },

{ apply fin.val_add }

lemma val_mul {n : ℕ} (a b : zmod n) : (a * b).val = (a.val * b.val) % n :=

cases n,

{ rw nat.mod_zero, apply int.nat_abs_mul },

{ apply fin.val_mul }

instance nontrivial (n : ℕ) [fact (1 < n)] : nontrivial (zmod n) :=

⟨⟨0, 1, assume 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 ⟩⟩

instance nontrivial' : nontrivial (zmod 0) := int.nontrivial

def inv : Π (n : ℕ), zmod n → zmod n

| 0 i := int.sign i

| (n+1) i := nat.gcd_a i.val (n+1)

instance (n : ℕ) : has_inv (zmod n) := ⟨inv n⟩

lemma inv_zero : ∀ (n : ℕ), (0 : zmod n)⁻¹ = 0

| 0 := int.sign_zero

| (n+1) := show (nat.gcd_a _ (n+1) : zmod (n+1)) = 0,

by { rw val_zero, unfold nat.gcd_a nat.xgcd nat.xgcd_aux, refl }

lemma mul_inv_eq_gcd {n : ℕ} (a : zmod n) :

a * a⁻¹ = nat.gcd a.val n :=

cases n,

{ calc a * a⁻¹ = a * int.sign a : rfl

... = a.nat_abs : by rw int.mul_sign

... = a.val.gcd 0 : by rw nat.gcd_zero_right; refl },

{ set k := n.succ,

calc a * a⁻¹ = a * a⁻¹ + k * nat.gcd_b (val a) k : by rw [nat_cast_self, zero_mul, add_zero]

... = ↑(↑a.val * nat.gcd_a (val a) k + k * nat.gcd_b (val a) k) :

by { push_cast, rw nat_cast_zmod_val, refl }

... = nat.gcd a.val k : (congr_arg coe (nat.gcd_eq_gcd_ab a.val k)).symm, }

@[simp] lemma nat_cast_mod (a : ℕ) (n : ℕ) : ((a % n : ℕ) : zmod n) = a :=

by conv {to_rhs, rw ← nat.mod_add_div a n}; simp

lemma eq_iff_modeq_nat (n : ℕ) {a b : ℕ} : (a : zmod n) = b ↔ a ≡ b [MOD n] :=

cases n,

{ simp only [nat.modeq, int.coe_nat_inj', nat.mod_zero], },

{ rw [fin.ext_iff, nat.modeq, ← val_nat_cast, ← val_nat_cast], exact iff.rfl, }

lemma coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : nat.coprime x n) :

(x * x⁻¹ : zmod n) = 1 :=

rw [nat.coprime, nat.gcd_comm, nat.gcd_rec] at h,

rw [mul_inv_eq_gcd, val_nat_cast, h, nat.cast_one],

def unit_of_coprime {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]⟩

@[simp] lemma coe_unit_of_coprime {n : ℕ} (x : ℕ) (h : nat.coprime x n) :

(unit_of_coprime x h : zmod n) = x := rfl

lemma val_coe_unit_coprime {n : ℕ} (u : (zmod n)ˣ) :

nat.coprime (u : zmod n).val n :=

cases 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_right_inv u),

rw [units.coe_one] at this,

rw [← eq_iff_modeq_nat, nat.cast_one, ← this], clear this,

rw [← nat_cast_zmod_val ((u * u⁻¹ : units (zmod (n+1))) : zmod (n+1))],

rw [units.coe_mul, val_mul, nat_cast_mod],

@[simp] lemma inv_coe_unit {n : ℕ} (u : (zmod n)ˣ) :

(u : zmod n)⁻¹ = (u⁻¹ : (zmod n)ˣ) :=

have := congr_arg (coe : ℕ → 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', { apply units.ext, refl },

rw h,

refl

lemma mul_inv_of_unit {n : ℕ} (a : zmod n) (h : is_unit a) :

a * a⁻¹ = 1 :=

rcases h with ⟨u, rfl⟩,

rw [inv_coe_unit, u.mul_inv],

lemma inv_mul_of_unit {n : ℕ} (a : zmod n) (h : is_unit a) :

a⁻¹ * a = 1 :=

by rw [mul_comm, mul_inv_of_unit a h]

def units_equiv_coprime {n : ℕ} [ne_zero n] : (zmod n)ˣ ≃ {x : zmod n // nat.coprime x.val n} :=

{ to_fun := λ x, ⟨x, val_coe_unit_coprime x⟩,

inv_fun := λ x, unit_of_coprime x.1.val x.2,

left_inv := λ ⟨_, _, _, _⟩, units.ext (nat_cast_zmod_val _),

right_inv := λ ⟨_, _⟩, by simp }

def chinese_remainder {m n : ℕ} (h : m.coprime n) :

zmod (m * n) ≃+* zmod m × zmod n :=

let to_fun : zmod (m * n) → zmod m × zmod n :=

zmod.cast_hom (show m.lcm n ∣ m * n, by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) in

let inv_fun : zmod m × zmod n → zmod (m * n) :=

λ x, if m * n = 0

then if m = 1

then ring_hom.snd _ _ x

else ring_hom.fst _ _ x

else nat.chinese_remainder h x.1.val x.2.val in

have inv : function.left_inverse inv_fun to_fun ∧ function.right_inverse inv_fun to_fun :=

if hmn0 : m * n = 0

then begin

rcases h.eq_of_mul_eq_zero hmn0 with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩;

simp [inv_fun, to_fun, function.left_inverse, function.right_inverse,

eq_int_cast, prod.ext_iff]

end

else

begin

haveI : ne_zero (m * n) := ⟨hmn0⟩,

haveI : ne_zero m := ⟨left_ne_zero_of_mul hmn0⟩,

haveI : ne_zero n := ⟨right_ne_zero_of_mul hmn0⟩,

have left_inv : function.left_inverse inv_fun to_fun,

{ intro x,

dsimp only [dvd_mul_left, dvd_mul_right, zmod.cast_hom_apply, coe_coe, inv_fun, to_fun],

conv_rhs { rw ← zmod.nat_cast_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.chinese_remainder h (x : zmod m).val (x : zmod n).val).2.left.trans _,

(nat.chinese_remainder h (x : zmod m).val (x : zmod n).val).2.right.trans _⟩,

{ rw [← zmod.eq_iff_modeq_nat, zmod.nat_cast_zmod_val, zmod.nat_cast_val] },

{ rw [← zmod.eq_iff_modeq_nat, zmod.nat_cast_zmod_val, zmod.nat_cast_val] } },

exact ⟨left_inv, left_inv.right_inverse_of_card_le (by simp)⟩,

end,

{ to_fun := to_fun,

inv_fun := inv_fun,

map_mul' := ring_hom.map_mul _,

map_add' := ring_hom.map_add _,

left_inv := inv.1,

right_inv := inv.2 }

instance subsingleton_units : subsingleton ((zmod 2)ˣ) :=

⟨dec_trivial⟩

lemma le_div_two_iff_lt_neg (n : ℕ) [hn : fact ((n : ℕ) % 2 = 1)]

{x : zmod n} (hx0 : x ≠ 0) : x.val ≤ (n / 2 : ℕ) ↔ (n / 2 : ℕ) < (-x).val :=

haveI npos : ne_zero n := ⟨by

{ unfreezingI { rintro rfl },

simpa [fact_iff] using hn, }⟩,

have hn2 : (n : ℕ) / 2 < n := nat.div_lt_of_lt_mul

((lt_mul_iff_one_lt_left $ ne_zero.pos n).2 dec_trivial),

have hn2' : (n : ℕ) - n / 2 = n / 2 + 1,

{ conv {to_lhs, congr, rw [← nat.succ_sub_one n, nat.succ_sub $ ne_zero.pos n]},

rw [← nat.two_mul_odd_div_two hn.1, two_mul, ← nat.succ_add, add_tsub_cancel_right], },

have hxn : (n : ℕ) - x.val < n,

{ rw [tsub_lt_iff_tsub_lt x.val_le le_rfl, tsub_self],

rw ← zmod.nat_cast_zmod_val x at hx0,

exact nat.pos_of_ne_zero (λ h, by simpa [h] using hx0) },

by conv {to_rhs, rw [← nat.succ_le_iff, nat.succ_eq_add_one, ← hn2', ← zero_add (- x),

← zmod.nat_cast_self, ← sub_eq_add_neg, ← zmod.nat_cast_zmod_val x,

← nat.cast_sub x.val_le,

zmod.val_nat_cast, nat.mod_eq_of_lt hxn, tsub_le_tsub_iff_left x.val_le] }

lemma ne_neg_self (n : ℕ) [hn : fact ((n : ℕ) % 2 = 1)] {a : zmod n} (ha : a ≠ 0) : a ≠ -a :=

λ h, have a.val ≤ n / 2 ↔ (n : ℕ) / 2 < (-a).val := le_div_two_iff_lt_neg n ha,

by rwa [← h, ← not_lt, not_iff_self] at this

lemma neg_one_ne_one {n : ℕ} [fact (2 < n)] :

(-1 : zmod n) ≠ 1 :=

char_p.neg_one_ne_one (zmod n) n

lemma neg_eq_self_mod_two (a : zmod 2) : -a = a :=

by fin_cases a; ext; simp [fin.coe_neg, int.nat_mod]; norm_num

@[simp] lemma nat_abs_mod_two (a : ℤ) : (a.nat_abs : zmod 2) = a :=

cases a,

{ simp only [int.nat_abs_of_nat, int.cast_coe_nat, int.of_nat_eq_coe] },

{ simp only [neg_eq_self_mod_two, nat.cast_succ, int.nat_abs, int.cast_neg_succ_of_nat] }

@[simp] lemma val_eq_zero : ∀ {n : ℕ} (a : zmod n), a.val = 0 ↔ a = 0

| 0 a := int.nat_abs_eq_zero

| (n+1) a := by { rw fin.ext_iff, exact iff.rfl }

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

rw [neg_eq_iff_add_eq_zero, ← two_mul],

cases n,

{ rw [@mul_eq_zero ℤ, @mul_eq_zero ℕ, val_eq_zero],

exact ⟨λ h, h.elim dec_trivial or.inl, λ h, or.inr (h.elim id $ λ h, h.elim dec_trivial id)⟩ },

conv_lhs

{ rw [← a.nat_cast_zmod_val, ← nat.cast_two, ← nat.cast_mul, nat_coe_zmod_eq_zero_iff_dvd] },

split,

{ rintro ⟨m, he⟩, cases 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 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, dec_trivial },

{ rintro (rfl|h), { rw [val_zero, mul_zero], apply dvd_zero }, { rw h } },

lemma val_cast_of_lt {n : ℕ} {a : ℕ} (h : a < n) : (a : zmod n).val = a :=

by rw [val_nat_cast, nat.mod_eq_of_lt h]

lemma neg_val' {n : ℕ} [ne_zero 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' _ (by rw [nat.modeq, ←val_add,

add_left_neg, tsub_add_cancel_of_le a.val_le, nat.mod_self, val_zero])

lemma neg_val {n : ℕ} [ne_zero n] (a : zmod n) : (-a).val = if a = 0 then 0 else n - a.val :=

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 (ne_zero.pos n),

contrapose! h,

rwa [le_zero_iff, val_eq_zero] at h,

def val_min_abs : Π {n : ℕ}, zmod n → ℤ

| 0 x := x

| n@(_+1) x := if x.val ≤ n / 2 then x.val else (x.val : ℤ) - n

@[simp] lemma val_min_abs_def_zero (x : zmod 0) : val_min_abs x = x := rfl

lemma val_min_abs_def_pos {n : ℕ} [ne_zero n] (x : zmod n) :

val_min_abs x = if x.val ≤ n / 2 then x.val else x.val - n :=

casesI n,

{ cases ne_zero.ne 0 rfl },

{ refl }

@[simp, norm_cast] lemma coe_val_min_abs : ∀ {n : ℕ} (x : zmod n), (x.val_min_abs : zmod n) = x

| 0 x := int.cast_id x

| k@(n+1) x :=

rw val_min_abs_def_pos,

split_ifs,

{ rw [int.cast_coe_nat, nat_cast_zmod_val] },

{ rw [int.cast_sub, int.cast_coe_nat, nat_cast_zmod_val, int.cast_coe_nat, nat_cast_self,

sub_zero] }

lemma injective_val_min_abs {n : ℕ} : (val_min_abs : zmod n → ℤ).injective :=

function.injective_iff_has_left_inverse.2 ⟨_, coe_val_min_abs⟩

lemma _root_.nat.le_div_two_iff_mul_two_le {n m : ℕ} : m ≤ n / 2 ↔ (m : ℤ) * 2 ≤ n :=

by rw [nat.le_div_iff_mul_le zero_lt_two, ← int.coe_nat_le, int.coe_nat_mul, nat.cast_two]

lemma val_min_abs_nonneg_iff {n : ℕ} [ne_zero n] (x : zmod n) :

0 ≤ x.val_min_abs ↔ x.val ≤ n / 2 :=

rw [val_min_abs_def_pos], split_ifs,

{ exact iff_of_true (nat.cast_nonneg _) h },

{ exact iff_of_false (sub_lt_zero.2 $ int.coe_nat_lt.2 x.val_lt).not_le h },

lemma val_min_abs_mul_two_eq_iff {n : ℕ} (a : zmod n) : a.val_min_abs * 2 = n ↔ 2 * a.val = n :=

cases n, { simp },

by_cases a.val ≤ n.succ / 2,

{ rw [val_min_abs, if_pos h, ← int.coe_nat_inj', nat.cast_mul, nat.cast_two, mul_comm] },

apply iff_of_false (λ he, _) (mt _ h),

{ rw [← a.val_min_abs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h,

exacts [h (nat.cast_nonneg _), zero_lt_two] },

{ rw [mul_comm], exact λ h, (nat.le_div_iff_mul_le zero_lt_two).2 h.le },

lemma val_min_abs_mem_Ioc {n : ℕ} [ne_zero n] (x : zmod n) :

x.val_min_abs * 2 ∈ set.Ioc (-n : ℤ) n :=

simp_rw [val_min_abs_def_pos, nat.le_div_two_iff_mul_two_le], split_ifs,

{ refine ⟨(neg_lt_zero.2 $ by exact_mod_cast ne_zero.pos n).trans_le (mul_nonneg _ _), h⟩,

exacts [nat.cast_nonneg _, zero_le_two] },

{ refine ⟨_, trans (mul_nonpos_of_nonpos_of_nonneg _ zero_le_two) $ nat.cast_nonneg _⟩,

{ linarith only [h] },

{ rw [sub_nonpos, int.coe_nat_le], exact x.val_lt.le } },

lemma val_min_abs_spec {n : ℕ} [ne_zero n] (x : zmod n) (y : ℤ) :

x.val_min_abs = y ↔ x = y ∧ y * 2 ∈ set.Ioc (-n : ℤ) n :=

⟨by { rintro rfl, exact ⟨x.coe_val_min_abs.symm, x.val_min_abs_mem_Ioc⟩ }, λ h, begin

rw ← sub_eq_zero,

apply @int.eq_zero_of_abs_lt_dvd n,

{ rw [← int_coe_zmod_eq_zero_iff_dvd, int.cast_sub, coe_val_min_abs, h.1, sub_self] },

rw [← mul_lt_mul_right (@zero_lt_two ℤ _ _ _ _ _)],

nth_rewrite 0 ← abs_eq_self.2 (@zero_le_two ℤ _ _ _ _),

rw [← abs_mul, sub_mul, abs_lt], split;

linarith only [x.val_min_abs_mem_Ioc.1, x.val_min_abs_mem_Ioc.2, h.2.1, h.2.2],

end⟩

lemma nat_abs_val_min_abs_le {n : ℕ} [ne_zero n] (x : zmod n) : x.val_min_abs.nat_abs ≤ n / 2 :=

rw [nat.le_div_two_iff_mul_two_le],

cases x.val_min_abs.nat_abs_eq,

{ rw ← h, exact x.val_min_abs_mem_Ioc.2 },

{ rw [← neg_le_neg_iff, ← neg_mul, ← h], exact x.val_min_abs_mem_Ioc.1.le },

@[simp] lemma val_min_abs_zero : ∀ n, (0 : zmod n).val_min_abs = 0

| 0 := by simp only [val_min_abs_def_zero]

| (n+1) := by simp only [val_min_abs_def_pos, if_true, int.coe_nat_zero, zero_le, val_zero]

@[simp] lemma val_min_abs_eq_zero {n : ℕ} (x : zmod n) :

x.val_min_abs = 0 ↔ x = 0 :=

cases n, { simp },

rw ← val_min_abs_zero n.succ,

apply injective_val_min_abs.eq_iff,

lemma nat_cast_nat_abs_val_min_abs {n : ℕ} [ne_zero n] (a : zmod n) :

(a.val_min_abs.nat_abs : zmod n) = if a.val ≤ (n : ℕ) / 2 then a else -a :=

have : (a.val : ℤ) - n ≤ 0,

by { erw [sub_nonpos, int.coe_nat_le], exact a.val_le, },

rw [val_min_abs_def_pos],

split_ifs,

{ rw [int.nat_abs_of_nat, nat_cast_zmod_val] },

{ rw [← int.cast_coe_nat, int.of_nat_nat_abs_of_nonpos this, int.cast_neg, int.cast_sub,

int.cast_coe_nat, int.cast_coe_nat, nat_cast_self, sub_zero, nat_cast_zmod_val], }

lemma val_min_abs_neg_of_ne_half {n : ℕ} {a : zmod n} (ha : 2 * a.val ≠ n) :

(-a).val_min_abs = -a.val_min_abs :=

casesI eq_zero_or_ne_zero n, { subst h, refl },

refine (val_min_abs_spec _ _).2 ⟨_, _, _⟩,

{ rw [int.cast_neg, coe_val_min_abs] },

{ rw [neg_mul, neg_lt_neg_iff],

exact a.val_min_abs_mem_Ioc.2.lt_of_ne (mt a.val_min_abs_mul_two_eq_iff.1 ha) },

{ linarith only [a.val_min_abs_mem_Ioc.1] },

@[simp] lemma nat_abs_val_min_abs_neg {n : ℕ} (a : zmod n) :

(-a).val_min_abs.nat_abs = a.val_min_abs.nat_abs :=

by_cases h2a : 2 * a.val = n,

{ rw a.neg_eq_self_iff.2 (or.inr h2a) },

{ rw [val_min_abs_neg_of_ne_half h2a, int.nat_abs_neg] }

lemma val_eq_ite_val_min_abs {n : ℕ} [ne_zero n] (a : zmod n) :

(a.val : ℤ) = a.val_min_abs + if a.val ≤ n / 2 then 0 else n :=

by { rw val_min_abs_def_pos, split_ifs; simp only [add_zero, sub_add_cancel] }

lemma prime_ne_zero (p q : ℕ) [hp : fact p.prime] [hq : fact q.prime] (hpq : p ≠ q) :

(q : zmod p) ≠ 0 :=

by rwa [← nat.cast_zero, ne.def, eq_iff_modeq_nat, nat.modeq_zero_iff_dvd,

← hp.1.coprime_iff_not_dvd, nat.coprime_primes hp.1 hq.1]

variables {n a : ℕ}

lemma val_min_abs_nat_abs_eq_min {n : ℕ} [hpos : ne_zero n] (a : zmod n) :

a.val_min_abs.nat_abs = min a.val (n - a.val) :=

rw val_min_abs_def_pos,

split_ifs with h h,

{ rw int.nat_abs_of_nat, symmetry,

apply min_eq_left (le_trans h (le_trans

(nat.half_le_of_sub_le_half _) (nat.sub_le_sub_left n h))),

rw nat.sub_sub_self (nat.div_le_self _ _) },

{ rw [←int.nat_abs_neg, neg_sub, ←nat.cast_sub a.val_le], symmetry,

apply min_eq_right (le_trans (le_trans (nat.sub_le_sub_left n (lt_of_not_ge h))

(nat.le_half_of_half_lt_sub _)) (le_of_not_ge h)),

rw nat.sub_sub_self (nat.div_lt_self (lt_of_le_of_ne' (nat.zero_le _) hpos.1) one_lt_two),

apply nat.lt_succ_self }

lemma val_min_abs_nat_cast_of_le_half (ha : a ≤ n / 2) : (a : zmod n).val_min_abs = a :=

cases n,

{ simp },

{ simp [val_min_abs_def_pos, val_nat_cast,

nat.mod_eq_of_lt (ha.trans_lt $ nat.div_lt_self' _ 0), ha] }

lemma val_min_abs_nat_cast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :

(a : zmod n).val_min_abs = a - n :=

cases n,

{ cases not_lt_bot ha' },

{ simp [val_min_abs_def_pos, val_nat_cast, nat.mod_eq_of_lt ha', ha.not_le] }

@[simp] lemma val_min_nat_abs_nat_cast_eq_self [ne_zero n] :

(a : zmod n).val_min_abs = a ↔ a ≤ n / 2 :=

refine ⟨λ ha, _, val_min_abs_nat_cast_of_le_half⟩,

rw [←int.nat_abs_of_nat a, ←ha],

exact nat_abs_val_min_abs_le a,

lemma nat_abs_min_of_le_div_two (n : ℕ) (x y : ℤ)

(he : (x : zmod n) = y) (hl : x.nat_abs ≤ n / 2) : x.nat_abs ≤ y.nat_abs :=

rw int_coe_eq_int_coe_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.nat_abs,

refine trans (trans ((add_le_add_iff_left _).2 hl) _) (int.nat_abs_sub_le _ _),

rw [add_sub_cancel, int.nat_abs_mul, int.nat_abs_of_nat],

refine trans _ (nat.le_mul_of_pos_right $ int.nat_abs_pos_of_ne_zero hm),

rw ← mul_two, apply nat.div_mul_le_self,

lemma nat_abs_val_min_abs_add_le {n : ℕ} (a b : zmod n) :

(a + b).val_min_abs.nat_abs ≤ (a.val_min_abs + b.val_min_abs).nat_abs :=

cases n, { refl },

apply nat_abs_min_of_le_div_two n.succ,

{ simp_rw [int.cast_add, coe_val_min_abs] },

{ apply nat_abs_val_min_abs_le },

variables (p : ℕ) [fact p.prime]

private lemma mul_inv_cancel_aux (a : zmod p) (h : a ≠ 0) : a * a⁻¹ = 1 :=

obtain ⟨k, rfl⟩ := nat_cast_zmod_surjective a,

apply coe_mul_inv_eq_one,

apply nat.coprime.symm,

rwa [nat.prime.coprime_iff_not_dvd (fact.out p.prime), ← char_p.cast_eq_zero_iff (zmod p)]

instance : field (zmod p) :=

{ mul_inv_cancel := mul_inv_cancel_aux p,

inv_zero := inv_zero p,

.. zmod.comm_ring p,

.. zmod.has_inv p,

.. zmod.nontrivial p }

instance (p : ℕ) [hp : fact p.prime] : is_domain (zmod p) :=

-- We need `cases p` here in order to resolve which `comm_ring` instance is being used.

unfreezingI { cases p, { exact (nat.not_prime_zero hp.out).elim }, },

exact @field.is_domain (zmod _) (zmod.field _)

end zmod