Commit 2024-03-24 08:10 8b3db4c3

View on Github →

feat(GroupTheory/FixedPointFree): New file (#11091) This PR adds a new file containing the definition of fixed-point-free automorphisms and some basic properties.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/BigOperators/Basic.lean

added theorem List.prod_range_div'

added theorem List.prod_range_div

Created Mathlib/GroupTheory/FixedPointFree.lean

added theorem MonoidHom.FixedPointFree.coe_eq_inv_of_involutive

added theorem MonoidHom.FixedPointFree.coe_eq_inv_of_sq_eq_one

added def MonoidHom.FixedPointFree.commGroupOfInvolutive

added theorem MonoidHom.FixedPointFree.commutatorMap_injective

added theorem MonoidHom.FixedPointFree.commutatorMap_surjective

added theorem MonoidHom.FixedPointFree.commute_all_of_involutive

added theorem MonoidHom.FixedPointFree.odd_card_of_involutive

added theorem MonoidHom.FixedPointFree.odd_orderOf_of_involutive

added theorem MonoidHom.FixedPointFree.orderOf_ne_two_of_involutive

added theorem MonoidHom.FixedPointFree.prod_pow_eq_one

added def MonoidHom.FixedPointFree

added def MonoidHom.commutatorMap

added theorem MonoidHom.commutatorMap_apply