Mathlib Map

Theorems · Theorem · group theory

AddMonoid.le_minOrder

∀ {α : Type u_2} [inst : AddMonoid α] {n : ℕ∞},
  n ≤ AddMonoid.minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 0 → IsOfFinAddOrder a → n ≤ ↑(addOrderOf a)
Defined in
Mathlib.GroupTheory.Order.Min
Cited by
2 results in Mathlib
Foundations
Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AddMonoid.le_minOrder_iff_forall_addSubgroup · cited by 2AddMonoid.le_minOrder_iff…AddMonoid.minOrder_le_addOrderOf · cited by 0AddMonoid.minOrder_le_add…ENat · cited by 4985ENatAddMonoid · cited by 2864AddMonoidaddOrderOf · cited by 208addOrderOfIsOfFinAddOrder · cited by 105IsOfFinAddOrderle_iInf_iff · cited by 30le_iInf_iffAddMonoid.minOrder · cited by 9AddMonoid.minOrderAddMonoid.le_minOrderCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.