Minimum order of an element

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

Main declarations

• Monoid.minOrder: The minimum order of an element of a given monoid.
• Monoid.minOrder_eq_top: The minimum order is infinite iff the monoid is torsion-free.
• ZMod.minOrder: The minimum order of $$\mathbb{Z}/n\mathbb{Z}$$ is the smallest factor of n, unless n = 0, 1.

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

• Monoid.minOrder α = ⨅ (a : α), ⨅ (_ : a ≠ 1), ⨅ (_ : IsOfFinOrder a), ↑(orderOf a)

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

• AddMonoid.minOrder α = ⨅ (a : α), ⨅ (_ : a ≠ 0), ⨅ (_ : IsOfFinAddOrder a), ↑(addOrderOf a)

@[simp]

theorem Monoid.minOrder_eq_top {α : Type u_1} [Monoid α] : minOrder α = ⊤ ↔ IsTorsionFree α

@[simp]

theorem AddMonoid.minOrder_eq_top {α : Type u_1} [AddMonoid α] : minOrder α = ⊤ ↔ IsTorsionFree α

@[simp]

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

Alias of the reverse direction of Monoid.minOrder_eq_top.

@[simp]

theorem AddMonoid.IsTorsionFree.minOrder {α : Type u_1} [AddMonoid α] : IsTorsionFree α → minOrder α = ⊤

@[simp]

theorem Monoid.le_minOrder {α : Type u_1} [Monoid α] {n : ℕ∞} : n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)

@[simp]

theorem AddMonoid.le_minOrder {α : Type u_1} [AddMonoid α] {n : ℕ∞} : n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 0 → IsOfFinAddOrder a → n ≤ ↑(addOrderOf a)

theorem Monoid.minOrder_le_orderOf {α : Type u_1} [Monoid α] {a : α} (ha : a ≠ 1) (ha' : IsOfFinOrder a) : minOrder α ≤ ↑(orderOf a)

theorem AddMonoid.minOrder_le_addOrderOf {α : Type u_1} [AddMonoid α] {a : α} (ha : a ≠ 0) (ha' : IsOfFinAddOrder a) : minOrder α ≤ ↑(addOrderOf a)

theorem Monoid.le_minOrder_iff_forall_subgroup {α : Type u_1} [Group α] {n : ℕ∞} : n ≤ minOrder α ↔ ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)

theorem AddMonoid.le_minOrder_iff_forall_addSubgroup {α : Type u_1} [AddGroup α] {n : ℕ∞} : n ≤ minOrder α ↔ ∀ ⦃s : AddSubgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)

theorem Monoid.minOrder_le_natCard {α : Type u_1} [Group α] {s : Subgroup α} (hs : s ≠ ⊥) (hs' : (↑s).Finite) : minOrder α ≤ ↑(Nat.card ↥s)

theorem AddMonoid.minOrder_le_natCard {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (hs : s ≠ ⊥) (hs' : (↑s).Finite) : minOrder α ≤ ↑(Nat.card ↥s)

@[simp]

theorem ZMod.minOrder {n : ℕ} (hn : n ≠ 0) (hn₁ : n ≠ 1) : AddMonoid.minOrder (ZMod n) = ↑n.minFac

@[simp]

theorem ZMod.minOrder_of_prime {p : ℕ} (hp : Nat.Prime p) : AddMonoid.minOrder (ZMod p) = ↑p