exponent_eq_iSup_orderOf' — Mathlib

English

In a commutative monoid, exponent G equals 0 if there exists an element with order 0; otherwise it equals the iSup of orders.

Русский

В коммутативном моноиде экспонента равна 0, если существует элемент порядка 0; иначе она равна iSup порядков.

LaTeX

$$$\\\\operatorname{exponent} G = \\\\text{ite}(\\\\exists g : G, \\\\operatorname{orderOf} g = 0)(0)(\\\\sup_{g : G} \\\\operatorname{orderOf} g)$$$

Lean4

@[to_additive]
theorem exponent_eq_iSup_orderOf' : exponent G = if ∃ g : G, orderOf g = 0 then 0 else ⨆ g : G, orderOf g :=
  by
  split_ifs with h
  · obtain ⟨g, hg⟩ := h
    exact exponent_eq_zero_of_order_zero hg
  · have := not_exists.mp h
    exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

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