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 $$ℤ/nℤ$$ is the smallest factor of n, unless n = 0, 1.

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)

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)

@[simp]

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

@[simp]

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

@[simp]

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

Alias of the reverse direction of Monoid.minOrder_eq_top.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem Monoid.minOrder_le_natCard {α : Type u_1} [Group α] {s : Subgroup α} (hs : s ≠ ⊥) (hs' : (↑s).Finite) : Monoid.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