Theorems · Definition · number theory

Nat.Partition.ofSymShapeEquiv

{n : ℕ} →
  {σ : Type u_1} →
    {τ : Type u_2} →
      [inst : DecidableEq σ] →
        [inst_1 : DecidableEq τ] →
          (μ : n.Partition) → σ ≃ τ → { x // Nat.Partition.ofSym x = μ } ≃ { x // Nat.Partition.ofSym x = μ }

An equivalence between σ and τ induces an equivalence between the subtypes of Sym σ n and Sym τ n corresponding to a given partition.

Defined in

Mathlib.Combinatorics.Enumerative.Partition.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEq