theorem ZMod.cast_int_add {n : ℕ} {x : ZMod n} {y : ZMod n} : ZMod.cast (x + y) = (ZMod.cast x + ZMod.cast y) % ↑n

theorem ZMod.cast_int_mul {n : ℕ} {x : ZMod n} {y : ZMod n} : ZMod.cast (x * y) = ZMod.cast x * ZMod.cast y % ↑n

theorem ZMod.cast_int_sub {n : ℕ} {x : ZMod n} {y : ZMod n} : ZMod.cast (x - y) = (ZMod.cast x - ZMod.cast y) % ↑n

theorem ZMod.cast_int_neg {n : ℕ} {x : ZMod n} : ZMod.cast (-x) = -ZMod.cast x % ↑n

theorem ZMod.val_one'' {n : ℕ} : n ≠ 1 → ZMod.val 1 = 1

@[simp]

theorem ZMod.inv_one (n : ℕ) : 1⁻¹ = 1

theorem ZMod.mul_val_inv {m : ℕ} {n : ℕ} (hmn : Nat.Coprime m n) : ↑m * ↑(ZMod.val (↑m)⁻¹) = 1

theorem ZMod.val_inv_mul {m : ℕ} {n : ℕ} (hmn : Nat.Coprime m n) : ↑(ZMod.val (↑m)⁻¹) * ↑m = 1

theorem ZMod.lift_injective {n : ℕ} {A : Type u_1} [AddCommGroup A] {f : { f : ℤ →+ A // f ↑n = 0 }} : Function.Injective ⇑((ZMod.lift n) f) ↔ ∀ (i : ℤ), ↑f i = 0 → ↑i = 0

@[simp]

theorem pow_zmod_val_inv_pow {α : Type u_1} [Group α] {n : ℕ} (hn : Nat.Coprime (Nat.card α) n) (a : α) : (a ^ ZMod.val (↑n)⁻¹) ^ n = a

@[simp]

theorem pow_pow_zmod_val_inv {α : Type u_1} [Group α] {n : ℕ} (hn : Nat.Coprime (Nat.card α) n) (a : α) : (a ^ n) ^ ZMod.val (↑n)⁻¹ = a

@[simp]

theorem nsmul_zmod_val_inv_nsmul {α : Type u_1} [AddGroup α] {n : ℕ} (hn : Nat.Coprime (Nat.card α) n) (a : α) : n • ZMod.val (↑n)⁻¹ • a = a

@[simp]

theorem zmod_val_inv_nsmul_nsmul {α : Type u_1} [AddGroup α] {n : ℕ} (hn : Nat.Coprime (Nat.card α) n) (a : α) : ZMod.val (↑n)⁻¹ • n • a = a