Documentation

Mathlib.GroupTheory.Order.Min

Minimum order of an element #

This file defines the minimum order of an element of a monoid.

Main declarations #

noncomputable def AddMonoid.minOrder (α : Type u_1) [AddMonoid α] :

The minimum order of a non-identity element. Also the minimum size of a nontrivial subgroup, see AddMonoid.le_minOrder_iff_forall_addSubgroup. Returns if the monoid is torsion-free.

Equations
Instances For
    noncomputable def Monoid.minOrder (α : Type u_1) [Monoid α] :

    The minimum order of a non-identity element. Also the minimum size of a nontrivial subgroup, see Monoid.le_minOrder_iff_forall_subgroup. Returns if the monoid is torsion-free.

    Equations
    Instances For
      @[simp]

      Alias of the reverse direction of Monoid.minOrder_eq_top.

      @[simp]
      theorem AddMonoid.le_minOrder {α : Type u_1} [AddMonoid α] {n : ℕ∞} :
      n AddMonoid.minOrder α ∀ ⦃a : α⦄, a 0IsOfFinAddOrder an (addOrderOf a)
      @[simp]
      theorem Monoid.le_minOrder {α : Type u_1} [Monoid α] {n : ℕ∞} :
      n Monoid.minOrder α ∀ ⦃a : α⦄, a 1IsOfFinOrder an (orderOf a)
      theorem AddMonoid.minOrder_le_addOrderOf {α : Type u_1} [AddMonoid α] {a : α} (ha : a 0) (ha' : IsOfFinAddOrder a) :
      theorem Monoid.minOrder_le_orderOf {α : Type u_1} [Monoid α] {a : α} (ha : a 1) (ha' : IsOfFinOrder a) :
      theorem AddMonoid.le_minOrder_iff_forall_addSubgroup {α : Type u_1} [AddGroup α] {n : ℕ∞} :
      n AddMonoid.minOrder α ∀ ⦃s : AddSubgroup α⦄, s Set.Finite sn (Nat.card s)
      theorem Monoid.le_minOrder_iff_forall_subgroup {α : Type u_1} [Group α] {n : ℕ∞} :
      n Monoid.minOrder α ∀ ⦃s : Subgroup α⦄, s Set.Finite sn (Nat.card s)
      theorem AddMonoid.minOrder_le_natCard {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (hs : s ) (hs' : Set.Finite s) :
      theorem Monoid.minOrder_le_natCard {α : Type u_1} [Group α] {s : Subgroup α} (hs : s ) (hs' : Set.Finite s) :
      @[simp]
      theorem ZMod.minOrder {n : } (hn : n 0) (hn₁ : n 1) :
      @[simp]
      theorem ZMod.minOrder_of_prime {p : } (hp : Nat.Prime p) :