English
Let m,n be natural numbers. In ZMod n, the residue of m, i.e. m mod n, is a unit if and only if gcd(m,n) = 1.
Русский
Пусть m,n натуральные числа. Остаток m по модулю n, то есть элемент m mod n, является обратимым в ZMod n тогда и только тогда, когда gcd(m,n) = 1.
LaTeX
$$$IsUnit\bigl(m : \mathbb{Z}/n\mathbb{Z}\bigr) \iff \gcd(m,n)=1$$$
Lean4
theorem isUnit_iff_coprime (m n : ℕ) : IsUnit (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
