Theorems · Theorem · ring theory
Finsupp.prod_congr
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {f : α →₀ M}
{g1 g2 : α → M → N}, (∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) → f.prod g1 = f.prod g2- Cited by
- 6 results in Mathlib
- Foundations
- Depth 60 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement · cited by 13,712
- Finsuppstatement and proof · cited by 5,255
- CommMonoidstatement and proof · cited by 2,264
- Finsupp.supportstatement and proof · cited by 828
- Finset.prod_congrproof · cited by 646
- Finsupp.prodstatement · cited by 231
Cited by6
Results whose statement or proof uses this declaration.
- Nat.totient_eq_prod_factorizationproof · cited by 2
- MvPowerSeries.prod_smul_X_eq_smul_monomial_oneproof · cited by 2
- MvPolynomial.aeval_ite_mem_eq_selfproof · cited by 1
- MvPolynomial.coeff_linearCombination_X_pow_of_fintypeproof · cited by 1
- Nat.totient_mul_prod_primeFactorsproof · cited by 1
- Finsupp.prod_mapDomain_indexproof · cited by 0