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 Monoid.minOrder (α : Type u_2) [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_2) [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.le_minOrder {α : Type u_2} [Monoid α] {n : ℕ∞} : n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)

@[simp]

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

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

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

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

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

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

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

@[simp]

theorem Monoid.minOrder_eq_top {G : Type u_1} [Group G] [IsMulTorsionFree G] : minOrder G = ⊤

@[simp]

theorem AddMonoid.minOrder_eq_top {G : Type u_1} [AddGroup G] [IsAddTorsionFree G] : minOrder G = ⊤

@[simp]

theorem Monoid.minOrder_eq_top_iff {G : Type u_1} [CommGroup G] : minOrder G = ⊤ ↔ IsMulTorsionFree G

@[simp]

theorem AddMonoid.minOrder_eq_top_iff {G : Type u_1} [AddCommGroup G] : minOrder G = ⊤ ↔ IsAddTorsionFree G

@[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