Theorems · Theorem · ring theory
Finsupp.prod_single_index
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {a : α} {b : M} {h : α → M → N},
h a 0 = 1 → (fun₀ | a => b).prod h = h a b- Cited by
- 26 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ZeroCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommMonoidstatement and proof · cited by 2,264
- Finsupp.singlestatement and proof · cited by 943
- Finsupp.prodstatement · cited by 231
- Finsupp.single_eq_sameproof · cited by 171
- Finset.mem_singletonproof · cited by 103
- Finset.prod_singletonproof · cited by 78
- Finsupp.support_single_subsetproof · cited by 27
- Finsupp.prod_of_support_subsetproof · cited by 13
Cited by26
Results whose statement or proof uses this declaration.
- MvPolynomial.eval₂_Xproof · cited by 36
- MvPolynomial.eval₂_mulproof · cited by 21
- wittPolynomial_eq_sum_C_mul_X_powproof · cited by 8
- MvPolynomial.eval₂_uniqueAlgEquivproof · cited by 4
- PowerSeries.coeff_substproof · cited by 4
- Nat.multiplicative_factorizationproof · cited by 3
- PowerSeries.rescale_eqproof · cited by 3
- aeval_wittPolynomialproof · cited by 3
- MvPolynomial.coeff_X_powproof · cited by 2
- MvPolynomial.eval₂_mul_monomialproof · cited by 2
- Subgroup.exists_finsupp_of_mem_closure_rangeproof · cited by 2
- Submonoid.exists_finsupp_of_mem_closure_rangeproof · cited by 2