exponent_eq_max'_orderOf — Mathlib

English

If there exists a multiplication-preserving equivalence between G and H, then the exponent of G equals the exponent of H.

Русский

Если существует эквивалентность умножения между G и H, экспонента сохраняется: exp(G) = exp(H).

LaTeX

$$$\\\\operatorname{exponent} G = \\\\operatorname{exponent} H$$$

Lean4

@[to_additive]
theorem exponent_eq_max'_orderOf [Fintype G] : exponent G = ((@Finset.univ G _).image orderOf).max' ⟨1, by simp⟩ :=
  by
  rw [← Finset.Nonempty.csSup_eq_max', Finset.coe_image, Finset.coe_univ, Set.image_univ, ← iSup]
  exact exponent_eq_iSup_orderOf orderOf_pos

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