isCyclic — Mathlib

English

If G ≃* G' is a multiplicative equivalence, then G is cyclic iff G' is cyclic.

Русский

Если существует мультипликативное эквивалентное отображение G ≃* G', то G циклична тогда и только тогда, когда G' циклична.

LaTeX

$$$IsCyclic(G) \iff IsCyclic(G')$$$

Lean4

@[to_additive]
theorem isCyclic (e : G ≃* G') : IsCyclic G ↔ IsCyclic G' :=
  ⟨fun _ ↦ isCyclic_of_surjective e e.surjective, fun _ ↦ isCyclic_of_surjective e.symm e.symm.surjective⟩

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