order_single — Mathlib

English

If r ≠ 0, then the order of the singleton (single a r) equals a.

Русский

Если r ≠ 0, то порядок одиночной Hahn-серии (\u2113 a r) равен a.

LaTeX

$$$ r \\neq 0 \\Rightarrow (\\mathrm{single}(a,r)).\\mathrm{order} = a $$$

Lean4

@[simp]
theorem order_single (h : r ≠ 0) : (single a r).order = a :=
  (order_of_ne (single_ne_zero h)).trans
    (support_single_subset ((single a r).isWF_support.min_mem (support_nonempty_iff.2 (single_ne_zero h))))

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