Monoid.IsTorsionFree.minOrder

theorem Monoid.IsTorsionFree.minOrder : ∀ {α : Type u_1} [inst : Monoid α], Monoid.IsTorsionFree α → Monoid.minOrder α = ⊤

The theorem `Monoid.IsTorsionFree.minOrder` states that for any given type `α` that forms a monoid, if the monoid is torsion-free (which means that the only element of the monoid that has finite order is the identity element), then the minimum order of a non-identity element in the monoid is infinity (`⊤`). In other words, there are no non-identity elements of finite order in a torsion-free monoid.

More concisely: In a torsion-free monoid, the order of every non-identity element is infinite.