Mathlib Map

Theorems · Theorem · combinatorics

Finset.coe_insert

∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), ↑(insert a s) = insert a ↑s
Defined in
Mathlib.Data.Finset.Insert
Cited by
124 results in Mathlib
Foundations
Depth 56 from the axioms, rests on 820 definitions · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEq
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MeasureTheory.SimpleFunc.induction · cited by 14SimpleFunc.inductionLinearIndependent.pair_iff · cited by 10LinearIndependent.pair_iffFinset.piecewise_insert · cited by 6Finset.piecewise_insertIdeal.height_le_spanRank_toENat_of_mem_minimalPrimes · cited by 5Ideal.height_le_spanRank_…MeasureTheory.IsSetRing.biUnion_mem · cited by 5IsSetRing.biUnion_memIdeal.subset_union_prime · cited by 4Ideal.subset_union_primeIdeal.prod_eq_iInf_of_pairwise_isCoprime · cited by 4Ideal.prod_eq_iInf_of_pai…LinearIndependent.pair_iff' · cited by 4LinearIndependent.pair_if…SimpleGraph.IsNClique.insert · cited by 3IsNClique.insertFinset.Ico_insert_right · cited by 3Finset.Ico_insert_rightMeasureTheory.integral_biUnion_finset · cited by 3MeasureTheory.integral_bi…linearIndepOn_isGroupLikeElem · cited by 3linearIndepOn_isGroupLike…Submodule.fg_induction · cited by 3Submodule.fg_inductionMeasureTheory.IsSetSemiring.isSetRing_supClosure · cited by 3IsSetSemiring.isSetRing_s…Finset.prod_dvd_of_coprime · cited by 3Finset.prod_dvd_of_coprimeSet · cited by 53352SetFinset · cited by 13712FinsetSetLike.coe · cited by 8199SetLike.coeFinset.coe_insertCITED 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 and proof · cited by 13,712
  • SetLike.coestatement · cited by 8,199

Cited by124

Results whose statement or proof uses this declaration.