English
There is a natural equivalence between the group of units of ZMod n and the subset of residues whose representatives are coprime to n.
Русский
Существует естественное биективное соответствие между группой единиц ZMod n и подмножеством резидьюсов, чьи представители взаимно просты с n.
LaTeX
$$$\text{Units}(\mathbb{Z}/n\mathbb{Z}) \cong \{ x : \mathbb{Z}/n\mathbb{Z} \mid \gcd(x, n)=1\} $$$
Lean4
/-- Equivalence between the units of `ZMod n` and
the subtype of terms `x : ZMod n` for which `x.val` is coprime to `n` -/
def unitsEquivCoprime {n : ℕ} [NeZero n] : (ZMod n)ˣ ≃ { x : ZMod n // Nat.Coprime x.val n }
where
toFun x := ⟨x, val_coe_unit_coprime x⟩
invFun x := unitOfCoprime x.1.val x.2
left_inv := fun ⟨_, _, _, _⟩ => Units.ext (natCast_zmod_val _)
right_inv := fun ⟨_, _⟩ => by simp
