Theorems · Theorem · number theory

Nat.Partition.ofSym.congr_simp

∀ {n : ℕ} {σ : Type u_1} (s s_1 : Sym σ n),
  s = s_1 → ∀ {inst : DecidableEq σ} [inst_1 : DecidableEq σ], Nat.Partition.ofSym s = Nat.Partition.ofSym s_1

Defined in: Mathlib.Combinatorics.Enumerative.Partition.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Symstatement and proof · cited by 150
Nat.Partitionstatement · cited by 36
Nat.Partition.ofSymstatement and proof · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.