Mathlib Map

Theorems · Theorem · combinatorics

Finset.coe_singleton

∀ {α : Type u_1} (a : α), ↑{a} = {a}
Defined in
Mathlib.Data.Finset.Insert
Cited by
145 results in Mathlib
Foundations
Depth 56 from the axioms, rests on 822 definitions · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Affine.Simplex.range_faceOpposite_points · cited by 30Simplex.range_faceOpposit…finsum_eq_single · cited by 18finsum_eq_singleFinset.map_singleton · cited by 15Finset.map_singletonMeasureTheory.SimpleFunc.induction · cited by 14SimpleFunc.inductionLinearIndependent.pair_iff · cited by 10LinearIndependent.pair_ifffg_adjoin_of_finite · cited by 9fg_adjoin_of_finiteFinsupp.comapDomain_single · cited by 9Finsupp.comapDomain_singleSubmodule.mem_span_finite_of_mem_span · cited by 6Submodule.mem_span_finite…MeasureTheory.IsSetRing.isSetSemiring · cited by 6IsSetRing.isSetSemiringMeasureTheory.addContent_mono · cited by 6MeasureTheory.addContent_…Finset.coe_zero · cited by 6Finset.coe_zeroMvPolynomial.mem_range_map_iff_coeffs_subset · cited by 5MvPolynomial.mem_range_ma…CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup · cited by 4CompleteLattice.isCompact…Function.locallyFinsuppWithin.logCounting_single_eq_log_sub_const · cited by 4locallyFinsuppWithin.logC…Finset.coe_one · cited by 4Finset.coe_oneSet · cited by 53352SetFinset · cited by 13712FinsetSetLike.coe · cited by 8199SetLike.coeFinset.coe_singletonCITED BYCITES

Cites3

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

  • Setstatement · cited by 53,352
  • Finsetstatement · cited by 13,712
  • SetLike.coestatement · cited by 8,199

Cited by145

Results whose statement or proof uses this declaration.