Coeff

📁 Source: Mathlib/Algebra/MvPolynomial/Coeff.lean

Statistics

Metric	Count
Definitions	0
Theorems coeff_add_pow, coeff_linearCombination_X_pow, coeff_linearCombination_X_pow_of_fintype, coeff_sum_X_pow_of_fintype	4
Total	4

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_add_pow 📖	mathematical	—	coeff MvPolynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass X AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Finset SetLike.instMembership Finset.instSetLike Finset.HasAntidiagonal.antidiagonal Finset.Nat.instHasAntidiagonal DFunLike.coe Finsupp.instFunLike Finset.decidableMem Nat.choose	—	Fin.sum_univ_two coeff_sum_X_pow_of_fintype Finsupp.sum_of_support_subset Finset.subset_univ Finsupp.multinomial_eq_of_support_subset Finset.univ_fin2 Nat.binomial_eq_choose
coeff_linearCombination_X_pow 📖	mathematical	—	coeff MvPolynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidAlgebra.addAddCommMonoid Finsupp.module Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike Finsupp.linearCombination X Finsupp.sum Nat.instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finsupp.multinomial Finsupp.prod CommSemiring.toCommMonoid Finsupp.instFunLike	—	—
coeff_linearCombination_X_pow_of_fintype 📖	mathematical	—	coeff MvPolynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Finset.sum AddMonoidAlgebra.addAddCommMonoid Finset.univ Algebra.toSMul AddMonoidAlgebra.algebra Algebra.id X Finsupp.sum Nat.instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finsupp.multinomial Finsupp.prod CommSemiring.toCommMonoid NonUnitalNonAssocSemiring.toMulZeroClass	—	Set.toFinite Subtype.finite Finite.of_fintype Finsupp.ofSupportFinite_coe Finsupp.prod_congr coeff_linearCombination_X_pow Finsupp.sum_of_support_subset zero_smul
coeff_sum_X_pow_of_fintype 📖	mathematical	—	coeff MvPolynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Finset.sum AddMonoidAlgebra.addAddCommMonoid Finset.univ X AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Finsupp.sum Nat.instAddCommMonoid Finsupp.multinomial	—	Finset.sum_congr one_smul coeff_linearCombination_X_pow_of_fintype one_pow Finsupp.prod_fun_one mul_one Nat.cast_ite Nat.cast_zero

---

← Back to Index