Theorems · Theorem · group theory
Finset.prod_erase_mul
∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι},
a ∈ s → (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f xA variant of Finset.mul_prod_erase with the multiplication swapped.
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoidDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- mul_commproof · cited by 2,262
- Finset.erasestatement and proof · cited by 455
- Finset.mul_prod_eraseproof · cited by 23
Cited by20
Results whose statement or proof uses this declaration.
- Finset.prod_eq_zeroproof · cited by 44
- Polynomial.prod_cyclotomic_eq_geom_sumproof · cited by 4
- Module.FinitePresentation.exists_lift_of_isLocalizedModuleproof · cited by 3
- Multiset.bell_mul_eqproof · cited by 2
- MeasureTheory.Measure.pi_map_evalproof · cited by 2
- Algebra.IsAlgebraic.exists_integral_multiplesproof · cited by 2
- Localization.exists_awayMap_bijective_of_localRingHom_bijectiveproof · cited by 1
- Finset.prod_erase_eq_divproof · cited by 1
- Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverseproof · cited by 1
- NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplexproof · cited by 1
- NumberField.mixedEmbedding.exists_primitive_element_lt_of_isRealproof · cited by 1
- AlgebraicGeometry.Proj.valuativeCriterion_existence_auxproof · cited by 1