case zero
u : (ZMod Nat.zero)ˣ
⊢ Nat.coprime (val ↑u) Nat.zero

case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ Nat.coprime (val ↑u) (Nat.succ n)
n : ℕ
u : (ZMod n)ˣ
⊢ Nat.coprime (val ↑u) n
cases' n with n
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ Nat.coprime (val ↑u) (Nat.succ n)
apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = ↑1
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
have := Units.ext_iff.1 (mul_right_inv u)
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = 1
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = ↑1
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
rw [Units.val_one] at this
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(u * u⁻¹)
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = 1
⊢ val ↑u * val ↑u⁻¹ ≡ 1 [MOD Nat.succ n]
rw [← eq_iff_modEq_nat, Nat.cast_one, ← this]
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(u * u⁻¹)
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(u * u⁻¹)
clear this
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(val ↑(u * u⁻¹))
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(u * u⁻¹)
rw [← nat_cast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]
no goals
case succ
n : ℕ
u : (ZMod (Nat.succ n))ˣ
⊢ ↑(val ↑u * val ↑u⁻¹) = ↑(val ↑(u * u⁻¹))
rw [Units.val_mul, val_mul, nat_cast_mod]
no goals
case zero
u : (ZMod Nat.zero)ˣ
⊢ Nat.coprime (val ↑u) Nat.zero
rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp