Theorems · Definition · group theory

Set.NSMul

{α : Type u_2} → [Zero α] → [Add α] → SMul ℕ (Set α)

Repeated pointwise addition (not the same as pointwise repeated addition!) of a Set. See note [pointwise nat action].

Defined in: Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by: 42 results in Mathlib
Foundations: Depth 7 from the axioms · uses no axioms
Assumes: Zero Add

Mathlib docs Source Loogle LeanSearch

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.

Setstatement and proof · cited by 53,352

Cited by45

Results whose statement or proof uses this declaration.

Set.addMonoidproof · cited by 18
Finset.coe_nsmulstatement · cited by 9
IsApproximateAddSubgroup.two_nsmul_covByVAddstatement · cited by 6
Set.nsmul_emptystatement · cited by 3
Set.nsmul_eq_emptystatement · cited by 2
Set.nsmul_singletonstatement · cited by 2
Set.nsmul_subset_nsmul_add_of_sq_subset_addstatement · cited by 2
Set.nsmul_subset_nsmul_leftstatement · cited by 2
Set.nsmul_subset_nsmul_rightstatement · cited by 2
Set.subset_nsmulstatement · cited by 2
AddSubgroup.nsmul_subsetstatement · cited by 2
AddSubmonoid.nsmul_subsetstatement · cited by 2