Theorems · Definition · group theory
MulEquiv.piMultiplicative
{ι : Type u_1} →
(K : ι → Type u_4) → [inst : (i : ι) → Add (K i)] → Multiplicative ((i : ι) → K i) ≃* ((i : ι) → Multiplicative (K i))Multiplicative (∀ i : ι, K i) is equivalent to ∀ i : ι, Multiplicative (K i).
- Defined in
- Mathlib.Algebra.Group.Equiv.TypeTags
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses Quot.sound
- Assumes
- Add
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.
- DFunLike.coeproof · cited by 62,936
- MulEquivstatement · cited by 1,142
- Multiplicativestatement and proof · cited by 875
- Multiplicative.ofAddproof · cited by 237
- Multiplicative.toAddproof · cited by 161
Cited by4
Results whose statement or proof uses this declaration.
- CommGroup.equiv_prod_multiplicative_zmod_of_finiteproof · cited by 1
- MulEquiv.funMultiplicativeproof · cited by 1
- MulEquiv.piMultiplicative_applystatement and proof · cited by 0
- MulEquiv.piMultiplicative_symm_applystatement and proof · cited by 0