one_lt_exponent — Mathlib

English

For a nontrivial finite cancellative monoid G, the exponent is greater than 1.

Русский

Для ненулевого конечного моноида с лево-отменяемостью экспонента больше 1.

LaTeX

$$$1 <\\\\operatorname{exponent} G$$$

Lean4

@[to_additive AddMonoid.one_lt_exponent]
theorem one_lt_exponent [Nontrivial G] : 1 < Monoid.exponent G :=
  by
  rw [Nat.one_lt_iff_ne_zero_and_ne_one]
  exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩

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