…ation (#17522)

This is the core of the work on the centralizer of a permutation.
It is the sequel of several PR which lay out basic useful results.

Let `α : Type` with `Fintype α` (and `DecidableEq α`).
The main goal of this file is to compute the cardinality of
conjugacy classes in `Equiv.Perm α`.
Every `g : Equiv.Perm α` has a `cycleType α : Multiset ℕ`.
By `Equiv.Perm.isConj_iff_cycleType_eq`,
two permutations are conjugate in `Equiv.Perm α` iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

A subsequent PR #17047 treats the case of the alternating group.



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

…ation (#17522)

This is the core of the work on the centralizer of a permutation.
It is the sequel of several PR which lay out basic useful results.

Let `α : Type` with `Fintype α` (and `DecidableEq α`).
The main goal of this file is to compute the cardinality of
conjugacy classes in `Equiv.Perm α`.
Every `g : Equiv.Perm α` has a `cycleType α : Multiset ℕ`.
By `Equiv.Perm.isConj_iff_cycleType_eq`,
two permutations are conjugate in `Equiv.Perm α` iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

A subsequent PR #17047 treats the case of the alternating group.



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

…ation (#17522)

This is the core of the work on the centralizer of a permutation.
It is the sequel of several PR which lay out basic useful results.

Let `α : Type` with `Fintype α` (and `DecidableEq α`).
The main goal of this file is to compute the cardinality of
conjugacy classes in `Equiv.Perm α`.
Every `g : Equiv.Perm α` has a `cycleType α : Multiset ℕ`.
By `Equiv.Perm.isConj_iff_cycleType_eq`,
two permutations are conjugate in `Equiv.Perm α` iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

A subsequent PR #17047 treats the case of the alternating group.



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

…ation (#17522)

This is the core of the work on the centralizer of a permutation.
It is the sequel of several PR which lay out basic useful results.

Let `α : Type` with `Fintype α` (and `DecidableEq α`).
The main goal of this file is to compute the cardinality of
conjugacy classes in `Equiv.Perm α`.
Every `g : Equiv.Perm α` has a `cycleType α : Multiset ℕ`.
By `Equiv.Perm.isConj_iff_cycleType_eq`,
two permutations are conjugate in `Equiv.Perm α` iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

A subsequent PR #17047 treats the case of the alternating group.



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

* factorial-dvd-int: (143 commits)
  Apply suggestions from code review
  feat(Factorial): k! divides the product of any k successive integers
  feat(CategoryTheory): creation of finite limits (#21320)
  chore: update Mathlib dependencies 2025-02-01 (#21328)
  chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314)
  feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306)
  chore: cleanup imports in Archive/IfNormalization (#21318)
  doc: fix several typos (#21315)
  feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310)
  chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271)
  feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084)
  chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308)
  feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522)
  feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168)
  chore: update Mathlib dependencies 2025-02-01 (#21312)
  chore: update Mathlib dependencies 2025-01-31 (#21311)
  feat: generalize `mem_dite` to `Membership α β` (#21262)
  feat: Lemmas for some monomial orders (#16177)
  feat(CategoryTheory): the localized category is monoidal (#12728)
  feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289)
  feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295)
  feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284)
  fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299)
  feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199)
  refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653)
  feat(RingTheory/PowerSeries): binomial series (#20192)
  chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff  (#21290)
  chore (RingTheory/HahnSeries): fix names that use coeff (#21279)
  feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233)
  chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273)
  feat(CategoryTheory): the monoidal category structure on a localization (#20951)
  feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009)
  feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328)
  feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486)
  feat: Function.const as a PartialEquiv (#21137)
  chore(NonZeroDivisors): don't import rings (#20871)
  feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267)
  feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190)
  feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285)
  perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179)
  feat(Order): order isomorphisms from `Fin n` for small `n` (#21120)
  refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740)
  feat: Sylow's first theorem for elementary `p`-groups (#21072)
  chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748)
  refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213)
  feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186)
  feat(Algebra/Group/Action): add definition of equidecomposition (#16936)
  feat(CategoryTheory/Subpresheaf): equalizer (#21096)
  feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204)
  chore: update Mathlib dependencies 2025-01-31 (#21282)
  ...

…ation (#17522)

This is the core of the work on the centralizer of a permutation.
It is the sequel of several PR which lay out basic useful results.

Let `α : Type` with `Fintype α` (and `DecidableEq α`).
The main goal of this file is to compute the cardinality of
conjugacy classes in `Equiv.Perm α`.
Every `g : Equiv.Perm α` has a `cycleType α : Multiset ℕ`.
By `Equiv.Perm.isConj_iff_cycleType_eq`,
two permutations are conjugate in `Equiv.Perm α` iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

A subsequent PR #17047 treats the case of the alternating group.



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

… centralizer of a permutation in the alternating group (#17047)

Let α : Type with Fintype α (and DecidableEq α).
The main goal of this file is to compute the cardinality of
conjugacy classes in `alternatingGroup α`.
Every g : Equiv.Perm α has a cycleType α : Multiset ℕ.
By Equiv.Perm.isConj_iff_cycleType_eq,
two permutations are conjugate in Equiv.Perm α iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.

This PR builds on the case of the full permutation group which is treated in #17522




Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>