Commit 2025-06-16 12:56 16c9f001

View on Github →

feat(GroupTheory): add Regular Wreath Product (#24816) feat: add regular wreath product and some results; add iterated wreath product; add the isomorphism of iterated wreath product of Z_p to sylow p subgroup of S_{p^n}. Needs some work simplifying final result.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/End.lean

added def Equiv.Perm.permCongrHom

Modified Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

added theorem Nat.Prime.multiplicity_factorial_pow

Created Mathlib/GroupTheory/RegularWreathProduct.lean

added theorem IteratedWreathProduct.card

added def IteratedWreathProduct

added theorem IteratedWreathProduct_succ

added theorem IteratedWreathProduct_zero

added theorem RegularWreathProduct.card

added def RegularWreathProduct.congr

added def RegularWreathProduct.equivProd

added theorem RegularWreathProduct.fun_id

added def RegularWreathProduct.inl

added theorem RegularWreathProduct.inv_left

added theorem RegularWreathProduct.inv_right

added theorem RegularWreathProduct.left_inl

added theorem RegularWreathProduct.mul_def

added theorem RegularWreathProduct.mul_left

added theorem RegularWreathProduct.mul_right

added theorem RegularWreathProduct.one_left

added theorem RegularWreathProduct.one_right

added def RegularWreathProduct.rightHom

added theorem RegularWreathProduct.rightHom_comp_inl_eq_id

added theorem RegularWreathProduct.rightHom_eq_right

added theorem RegularWreathProduct.right_inl

added theorem RegularWreathProduct.smul_def

added def RegularWreathProduct.toPerm

added theorem RegularWreathProduct.toPermInj

added structure RegularWreathProduct

added def iteratedWreathToPermHom

added theorem iteratedWreathToPermHomInj

Modified Mathlib/Logic/Equiv/Fin/Basic.lean

added def Fin.succFunEquiv

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem Nat.card_fin