English
If u ∈ (ZMod n)ˣ, then gcd((u : ZMod n).val, n) = 1, i.e., Nat.Coprime ((u : ZMod n).val) n.
Русский
Пусть u ∈ (ZMod n)ˣ; тогда gcd((u : ZMod n).val, n) = 1, то есть Nat.Coprime ((u : ZMod n).val) n.
LaTeX
$$$\text{Nat.Coprime}((u : ZMod n).val, n)$$$
Lean4
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 [← natCast_eq_natCast_iff, 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]
