isCyclic_units_two_pow_iff — Mathlib

English

For natural n, the unit group of ZMod(2^n) is cyclic if and only if n ≤ 2.

Русский

Для натурального n группа единиц ZMod(2^n) циклична тогда и только тогда, когда n ≤ 2.

LaTeX

$$$\\\\IsCyclic\\\\left((\\\\mathbb{Z}/2^{n}\\\\mathbb{Z})^{\\\\times}\\\\right) \\\\Leftrightarrow n \\\\le 2.$$$

Lean4

theorem isCyclic_units_two_pow_iff (n : ℕ) : IsCyclic (ZMod (2 ^ n))ˣ ↔ n ≤ 2 := by
  match n with
  | 0 => simp [isCyclic_units_one]
  | 1 => simp [isCyclic_units_prime Nat.prime_two]
  | 2 => simp [isCyclic_units_four]
  | n + 3 =>
    simp only [Nat.reduceLeDiff, iff_false]
    intro H
    apply not_isCyclic_units_eight
    have h : 2 ^ 3 ∣ 2 ^ (n + 3) := pow_dvd_pow _ (by cutsat)
    exact isCyclic_of_surjective _ (unitsMap_surjective h)

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