exists_pow_ne_one_of_isCyclic — Mathlib

English

If there is an injective monoid homomorphism f : F →* G' and G' is cyclic, then G is cyclic.

Русский

Если существует инъективный моноид-гомоморфизм f: F →* G' и G' циклична, то G циклична.

LaTeX

$$IsCyclic(G) при наличии f : F →* G' инъективного и IsCyclic(G')$$

Lean4

@[to_additive]
theorem exists_pow_ne_one_of_isCyclic [G_cyclic : IsCyclic G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) :
    ∃ a : G, a ^ k ≠ 1 :=
  by
  have : Finite G := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt k_lt_card_G)
  rcases G_cyclic with ⟨a, ha⟩
  use a
  contrapose! k_lt_card_G
  convert orderOf_le_of_pow_eq_one k_pos.bot_lt k_lt_card_G
  rw [← Nat.card_zpowers, eq_comm, card_eq_iff_eq_top, eq_top_iff]
  exact fun x _ ↦ ha x

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