Mathlib Map

Theorems · Theorem · group theory

Set.singleton_pow

∀ {α : Type u_2} [inst : Monoid α] (a : α) (n : ℕ), {a} ^ n = {a ^ n}
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
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.pow_mem_pow · cited by 2Set.pow_mem_powSet.singleton_zpow · cited by 0Set.singleton_zpowSet · cited by 53352SetMonoid · cited by 3887MonoidSet.NPow · cited by 51Set.NPowSet.singleton_powCITED 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
  • Monoidstatement and proof · cited by 3,887
  • Set.NPowstatement · cited by 51

Cited by2

Results whose statement or proof uses this declaration.