Mathlib Map

Theorems · Theorem · group theory

Set.nsmul_singleton

∀ {α : Type u_2} [inst : AddMonoid α] (a : α) (n : ℕ), n • {a} = {n • a}
Defined in
Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by
2 results in Mathlib
Foundations
Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.nsmul_mem_nsmul · cited by 1Set.nsmul_mem_nsmulSet.zsmul_singleton · cited by 0Set.zsmul_singletonSet · cited by 53352SetAddMonoid · cited by 2864AddMonoidSet.NSMul · cited by 42Set.NSMulSet.nsmul_singletonCITED 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
  • AddMonoidstatement and proof · cited by 2,864
  • Set.NSMulstatement · cited by 42

Cited by2

Results whose statement or proof uses this declaration.