isCyclic_units_two_mul_iff_of_odd

English

If n is odd, then IsCyclic((ZMod(2n))×) iff IsCyclic((ZMod(n))×).

Русский

Если n нечетно, то IsCyclic((ZMod(2n))×) эквивалентно IsCyclic((ZMod(n))×).

LaTeX

$$$\\\\IsCyclic\\\\left((\\\\mathbb{Z}/(2n)\\\\mathbb{Z})^{\\\\times}\\\\right) \\\\Leftrightarrow \\\\IsCyclic\\\\left((\\\\mathbb{Z}/n\\\\mathbb{Z})^{\\\\times}\\\\right), \\\\text{ если } n \\\\text{ нечетно}. $$$$

Lean4

theorem isCyclic_units_two_mul_iff_of_odd (n : ℕ) (hn : Odd n) : IsCyclic (ZMod (2 * n))ˣ ↔ IsCyclic (ZMod n)ˣ := by
  simp [((Units.mapEquiv (chineseRemainder <| Nat.coprime_two_left.mpr hn).toMulEquiv).trans .prodUnits).isCyclic,
    Group.isCyclic_prod_iff, isCyclic_units_two]

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