Mathlib Map

Theorems · Definition · group theory

Finset.zero

{α : Type u_2} → [Zero α] → Zero (Finset α)

The finset 0 : Finset α is defined as {0} in scope Pointwise.

Defined in
Mathlib.Algebra.Group.Pointwise.Finset.Basic
Cited by
74 results in Mathlib
Foundations
Depth 25 from the axioms · uses propext, Quot.sound
Assumes
Zero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finsupp.rangeIcc · cited by 6Finsupp.rangeIccFinset.coe_zero · cited by 6Finset.coe_zeroFinset.zero_nonempty · cited by 6Finset.zero_nonemptyDFinsupp.rangeIcc · cited by 5DFinsupp.rangeIccFinset.mem_zero · cited by 4Finset.mem_zeroFinsupp.rangeSingleton · cited by 3Finsupp.rangeSingletonFinset.card_zero · cited by 3Finset.card_zeroFinset.image_zero · cited by 3Finset.image_zeroFinset.zero_mem_zero · cited by 3Finset.zero_mem_zeroFinset.inv_zero · cited by 2Finset.inv_zeroDFinsupp.pi · cited by 2DFinsupp.piFinset.singletonZeroHom · cited by 2Finset.singletonZeroHomFinsupp.pi · cited by 2Finsupp.piFinset.zero_smul_finset · cited by 2Finset.zero_smul_finsetFinset.zero_subset · cited by 2Finset.zero_subsetFinset · cited by 13712FinsetFinset.zeroCITED BYCITES

Cites1

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

  • Finsetstatement · cited by 13,712

Cited by83

Results whose statement or proof uses this declaration.