Mathlib Map

Theorems · Definition · group theory

Finset.zpow

{α : Type u_2} → [DecidableEq α] → [One α] → [Mul α] → [Inv α] → Pow (Finset α) ℤ

Repeated pointwise multiplication/division (not the same as pointwise repeated multiplication/division!) of a Finset. See note [pointwise nat action].

Defined in
Mathlib.Algebra.Group.Pointwise.Finset.Basic
Cited by
6 results in Mathlib
Foundations
Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEqOneMulInv
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.empty_zpow · cited by 2Finset.empty_zpowFinset.Nonempty.zpow · cited by 1Nonempty.zpowFinset.singleton_zpow · cited by 0Finset.singleton_zpowFinset.zpow_eq_empty · cited by 0Finset.zpow_eq_emptyFinset.coe_zpow · cited by 0Finset.coe_zpowFinset.small_alternating_pow_of_small_tripling · cited by 0Finset.small_alternating_…Finset · cited by 13712FinsetzpowRec · cited by 1zpowRecFinset.zpowCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Finsetstatement and proof · cited by 13,712
  • zpowRecproof · cited by 1

Cited by6

Results whose statement or proof uses this declaration.