Theorems · Theorem · group theory
orderOf_map_dvd
∀ {G : Type u_1} [inst : Monoid G] {H : Type u_6} [inst_1 : Monoid H] (ψ : G →* H) (x : G), orderOf (ψ x) ∣ orderOf x- Defined in
- Mathlib.GroupTheory.OrderOfElement
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- map_oneproof · cited by 861
- map_powproof · cited by 503
- orderOfstatement and proof · cited by 324
- pow_orderOf_eq_oneproof · cited by 30
- orderOf_dvd_of_pow_eq_oneproof · cited by 24
Cited by3
Results whose statement or proof uses this declaration.
- ZMod.isCyclic_units_of_prime_powproof · cited by 2
- MonoidHom.independent_range_of_coprime_orderproof · cited by 1
- IsPGroup.smul_mul_inv_trivial_or_surjectiveproof · cited by 1