Mathlib Map

Theorems · Theorem · combinatorics

Finset.sym_empty

∀ {α : Type u_1} [inst : DecidableEq α] (n : ℕ), ∅.sym (n + 1) = ∅
Defined in
Mathlib.Data.Finset.Sym
Cited by
1 results in Mathlib
Foundations
Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEq
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.sym_eq_empty · cited by 2Finset.sym_eq_emptyFinset · cited by 13712FinsetSym · cited by 150SymFinset.sym · cited by 35Finset.symFinset.sym_emptyCITED BYCITES

Cites3

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

  • Finsetstatement · cited by 13,712
  • Symstatement · cited by 150
  • Finset.symstatement · cited by 35

Cited by1

Results whose statement or proof uses this declaration.