minOrder — Mathlib

English

For ZMod n with n ≠ 0,1, the minimum order of a nontrivial element equals the least factor of n, i.e., n.minFac cast to the additive order.

Русский

Для ZMod n, при n ≠ 0,1, минимальный порядок ненулевого элемента равен наименьшему делителю n (minFac), приведённому к порядку в ZMod.

LaTeX

$$$n \neq 0,\ n \neq 1 \Rightarrow \minOrder(\mathbb{Z}/n\mathbb{Z}) = (n.minFac)^{\text{cast}}$$$

Lean4

@[simp]
protected theorem minOrder {n : ℕ} (hn : n ≠ 0) (hn₁ : n ≠ 1) : minOrder (ZMod n) = n.minFac :=
  by
  have : Fact (1 < n) := ⟨one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn, hn₁⟩⟩
  classical
  have : (↑(n / n.minFac) : ZMod n) ≠ 0 :=
    by
    rw [Ne, ringChar.spec, ringChar.eq (ZMod n) n]
    exact
      not_dvd_of_pos_of_lt (Nat.div_pos (minFac_le hn.bot_lt) n.minFac_pos)
        (div_lt_self hn.bot_lt (minFac_prime hn₁).one_lt)
  refine
    ((minOrder_le_natCard (zmultiples_eq_bot.not.2 this) <| toFinite _).trans ?_).antisymm <|
      le_minOrder_iff_forall_addSubgroup.2 fun s hs _ ↦ ?_
  ·
    rw [Nat.card_zmultiples, ZMod.addOrderOf_coe _ hn, gcd_eq_right (div_dvd_of_dvd n.minFac_dvd),
      Nat.div_div_self n.minFac_dvd hn]
  · haveI : Nontrivial s := s.bot_or_nontrivial.resolve_left hs
    exact
      WithTop.coe_le_coe.2 <| minFac_le_of_dvd Finite.one_lt_card <| (card_addSubgroup_dvd_card _).trans n.card_zmod.dvd

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