Theorems · Definition · group theory
Finset.smulFinset
{α : Type u_2} → {β : Type u_3} → [DecidableEq β] → [SMul α β] → SMul α (Finset β)The scaling of a finset s by a scalar a: a • s = {a • x | x ∈ s}.
- Cited by
- 101 results in Mathlib
- Foundations
- Depth 74 from the axioms, rests on 1,343 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqSMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Finset.imageproof · cited by 910
Cited by102
Results whose statement or proof uses this declaration.
- Finset.coe_smul_finsetstatement · cited by 16
- Finset.card_smul_finsetstatement · cited by 12
- Finset.card_inter_smulstatement · cited by 5
- Finset.smul_finset_interstatement · cited by 4
- Finset.smul_mem_smul_finset_iffstatement · cited by 4
- Finset.smul_finset_univstatement · cited by 3
- Finset.mem_smul_finsetstatement · cited by 3
- Finset.inv_smul_mem_iffstatement · cited by 3
- Equiv.Perm.support_conj_eq_smul_supportstatement · cited by 3
- Finset.card_smul_interstatement · cited by 3
- Finset.card_smul_inter_smulstatement · cited by 3
- Finset.smul_finset_subset_mulstatement · cited by 2