Theorems · Definition · group theory

monoidHomOfForallMemZpowers

{G : Type u_2} →
  {G' : Type u_3} →
    [inst : Group G] →
      [inst_1 : Group G'] → {g : G} → (∀ (x : G), x ∈ Subgroup.zpowers g) → {g' : G'} → orderOf g' ∣ orderOf g → G →* G'

If g generates the group G and g' is an element of another group G' whose order divides that of g, then there is a homomorphism G →* G' mapping g to g'.

Defined in

Mathlib.GroupTheory.SpecificGroups.Cyclic

Cited by

4 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroup