Commit 2024-06-01 05:50 30a8ef8d

View on Github →

feat(GroupTheory/SpecificGroups/Cyclic): add material on groups with given generator (#13423) This adds some material to Mathlib.GroupTheory.SpecificGroups.Cyclic for dealing with groups that have a specified generator, mostly on existence and uniqueness of homomorphisms and isomorphisms in terms of the image of the given generator.

Estimated changes

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem MonoidHom.eq_iff_eq_on_generator

added theorem MulEquiv.eq_iff_eq_on_generator

added def monoidHomOfForallMemZpowers

added theorem monoidHomOfForallMemZpowers_apply_gen

added def mulEquivOfOrderOfEq

added theorem mulEquivOfOrderOfEq_apply_gen

added theorem mulEquivOfOrderOfEq_symm

added theorem mulEquivOfOrderOfEq_symm_apply_gen

added theorem orderOf_generator_eq_natCard