Theorems · Definition · group theory
Finset.one
{α : Type u_2} → [One α] → One (Finset α)The finset 1 : Finset α is defined as {1} in scope Pointwise.
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
- Assumes
- One
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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 by45
Results whose statement or proof uses this declaration.
- Finset.coe_onestatement · cited by 4
- Finset.one_nonemptystatement · cited by 4
- Finset.card_onestatement · cited by 3
- Finset.image_onestatement · cited by 3
- Finset.singletonOneHomstatement · cited by 2
- Finset.imageOneHomstatement · cited by 1
- Finset.coe_list_prodstatement · cited by 1
- Finset.preimage_mul_left_onestatement · cited by 1
- Finset.preimage_mul_right_onestatement · cited by 1
- MonoidAlgebra.support_coeff_onestatement · cited by 1
- MonoidAlgebra.support_coeff_one_subsetstatement · cited by 1
- Finset.one_mem_onestatement · cited by 1