exp_eq_one_iff — Mathlib

English

For a Monoid G, exponent(G) = 1 iff G is subsingleton.

Русский

Для моноида G экспонента равна 1 тогда и только тогда, когда G–пододин.

LaTeX

$$$\\operatorname{exponent}(G)=1 \\iff \\text{Subsingleton}(G)$$$

Lean4

@[to_additive AddMonoid.exp_eq_one_iff]
theorem exp_eq_one_iff : exponent G = 1 ↔ Subsingleton G :=
  by
  refine ⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩
  · rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]
  · apply exponent_min' _ Nat.one_pos
    simp [eq_iff_true_of_subsingleton]
  · apply Nat.succ_le_of_lt
    apply exponent_pos_of_exists 1 Nat.one_pos
    simp [eq_iff_true_of_subsingleton]

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