zmodCyclicMulEquiv — Mathlib

English

There is an isomorphism between Multiplicative ZMod n and any cyclic group of order n.

Русский

Существует изоморфизм между мультипликативной ZMod n и любой циклической группой порядка n.

LaTeX

$$$\text{MulInv}(\mathbb{Z}/n\mathbb{Z}) \cong^* G$ для любой циклической группы $G$ с $|G|=n$.$$

Lean4

/-- The isomorphism from `Multiplicative (ZMod n)` to any cyclic group of `Nat.card` equal to `n`.
-/
noncomputable def zmodCyclicMulEquiv [Group G] (h : IsCyclic G) : Multiplicative (ZMod (Nat.card G)) ≃* G :=
  AddEquiv.toMultiplicative <| zmodAddCyclicAddEquiv <| isAddCyclic_additive_iff.2 h

Похожие утверждения