Mathlib Map

Theorems · Theorem · group theory

orderOf_le_card_univ

∀ {G : Type u_1} [inst : Monoid G] {x : G} [inst_1 : Fintype G], orderOf x ≤ Fintype.card G
Defined in
Mathlib.GroupTheory.OrderOfElement
Cited by
3 results in Mathlib
Foundations
Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
MonoidFintype
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

lucas_primality · cited by 2lucas_primalityorderOf_le_card · cited by 2orderOf_le_cardLucasLehmer.order_ineq · cited by 1LucasLehmer.order_ineqFintype · cited by 7736FintypeMonoid · cited by 3887MonoidFintype.card · cited by 1386Fintype.cardFinset.mem_univ · cited by 361Finset.mem_univorderOf · cited by 324orderOfFinset.le_card_of_inj_on_range · cited by 3Finset.le_card_of_inj_on_…pow_injOn_Iio_orderOf · cited by 2pow_injOn_Iio_orderOforderOf_le_card_univCITED BYCITES

Cites7

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

Cited by3

Results whose statement or proof uses this declaration.