Theorems · Theorem · group theory

Fintype.piFinset_inv

∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Inv (α i)] (s : (i : ι) → Finset (α i)),
  (Fintype.piFinset fun i => (s i)⁻¹) = (Fintype.piFinset s)⁻¹

Defined in: Mathlib.Algebra.Group.Pointwise.Finset.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableEq DecidableEq Inv

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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
Fintypestatement and proof · cited by 7,736
Fintype.piFinsetstatement · cited by 86
Finset.invstatement · cited by 70
Fintype.piFinset_imageproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.