Theorems · Theorem · group theory
Finset.prod_congr
∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f g : ι → M},
s₁ = s₂ → (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g- Cited by
- 646 results in Mathlib
- Foundations
- Depth 55 from the axioms, rests on 839 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Finset.prodstatement and proof · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Finset.fold_congrproof · cited by 11
Cited by646
Results whose statement or proof uses this declaration.
- Multipliable.hasProdproof · cited by 88
- Matrix.det_mulproof · cited by 51
- FormalMultilinearSeries.coeff_ofScalarsproof · cited by 23
- Finset.prod_eq_oneproof · cited by 22
- finprod_eq_prod_of_mulSupport_subsetproof · cited by 21
- Fin.prod_univ_twoproof · cited by 16
- Matrix.det_uniqueproof · cited by 15
- Polynomial.prod_cyclotomic_eq_X_pow_sub_oneproof · cited by 11
- Polynomial.resultant_commproof · cited by 11
- Matrix.det_fromBlocks_zero₂₁proof · cited by 10
- Fin.prod_univ_castSuccproof · cited by 10
- Finset.prod_sigmaproof · cited by 10
Showing the 200 most cited of 646.