Support

📁 Source: Mathlib/Algebra/Polynomial/Degree/Support.lean

Statistics

Metric	Count
Definitions	0
Theorems as_sum_range, as_sum_range', as_sum_range_C_mul_X_pow, as_sum_range_C_mul_X_pow', as_sum_support, as_sum_support_C_mul_X_pow, card_supp_le_succ_natDegree, card_support_C_mul_X_pow_le_one, le_degree_of_mem_supp, le_natDegree_of_mem_supp, mem_support_C_mul_X_pow, natDegree_eq_support_max', natDegree_mem_support_of_nonzero, nonempty_support_iff, sum_fin, sum_over_range, sum_over_range', supDegree_eq_natDegree, supp_subset_range, supp_subset_range_natDegree_succ	20
Total	20

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
as_sum_range 📖	mathematical	—	Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Finset.range natDegree DFunLike.coe LinearMap RingHom.id Semiring.toModule module LinearMap.instFunLike monomial coeff	—	as_sum_range' lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
as_sum_range' 📖	mathematical	natDegree	Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Finset.range DFunLike.coe LinearMap RingHom.id Semiring.toModule module LinearMap.instFunLike monomial coeff	—	sum_monomial_eq sum_over_range' monomial_zero_right
as_sum_range_C_mul_X_pow 📖	mathematical	—	Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Finset.range natDegree instMul DFunLike.coe RingHom RingHom.instFunLike C coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	as_sum_range_C_mul_X_pow' lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
as_sum_range_C_mul_X_pow' 📖	mathematical	natDegree	Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Finset.range instMul DFunLike.coe RingHom RingHom.instFunLike C coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	as_sum_range' Finset.sum_congr C_mul_X_pow_eq_monomial
as_sum_support 📖	mathematical	—	Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring support DFunLike.coe LinearMap RingHom.id Semiring.toModule module LinearMap.instFunLike monomial coeff	—	sum_monomial_eq
as_sum_support_C_mul_X_pow 📖	mathematical	—	Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring support instMul DFunLike.coe RingHom RingHom.instFunLike C coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv as_sum_support Finset.sum_congr C_mul_X_pow_eq_monomial
card_supp_le_succ_natDegree 📖	mathematical	—	Finset.card support natDegree	—	Finset.card_range Finset.card_le_card supp_subset_range_natDegree_succ
card_support_C_mul_X_pow_le_one 📖	mathematical	—	Finset.card support Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	Finset.card_singleton Finset.card_le_card support_C_mul_X_pow'
le_degree_of_mem_supp 📖	mathematical	Finset Finset.instMembership support	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne degree	—	le_degree_of_ne_zero mem_support_iff
le_natDegree_of_mem_supp 📖	mathematical	Finset Finset.instMembership support	natDegree	—	le_natDegree_of_ne_zero mem_support_iff
mem_support_C_mul_X_pow 📖	—	Finset Finset.instMembership support Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	—	Finset.mem_singleton support_C_mul_X_pow'
natDegree_eq_support_max' 📖	mathematical	—	natDegree Finset.max' Nat.instLinearOrder support Finset.Nonempty Polynomial instZero nonempty_support_iff	—	LE.le.antisymm natDegree_mem_support_of_nonzero Finset.le_max' Finset.max'_le le_natDegree_of_mem_supp
natDegree_mem_support_of_nonzero 📖	mathematical	—	Finset Finset.instMembership support natDegree	—	mem_support_iff leadingCoeff_eq_zero
nonempty_support_iff 📖	mathematical	—	Finset.Nonempty support	—	Finset.nonempty_iff_ne_empty support_eq_empty
sum_fin 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne	Finset.sum Finset.univ Fin.fintype coeff sum	—	sum_zero_index Finset.sum_eq_zero sum_over_range' natDegree_lt_iff_degree_lt Fin.sum_univ_eq_sum_range
sum_over_range 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum Finset.sum Finset.range natDegree coeff	—	sum_over_range' lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
sum_over_range' 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid natDegree	sum Finset.sum Finset.range coeff	—	supp_subset_range Finset.sum_congr Finsupp.sum_of_support_subset
supDegree_eq_natDegree 📖	mathematical	—	AddMonoidAlgebra.supDegree Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat Nat.instOrderBot toFinsupp natDegree	—	eq_or_ne AddMonoidAlgebra.supDegree_zero WithBot.coe_injective AddMonoidAlgebra.supDegree_withBot_some_comp support_toFinsupp Finset.nonempty_iff_ne_empty support_eq_empty supDegree_eq_degree degree_eq_natDegree Nat.cast_withBot
supp_subset_range 📖	mathematical	natDegree	Finset Finset.instHasSubset support Finset.range	—	Finset.mem_range LE.le.trans_lt le_natDegree_of_mem_supp
supp_subset_range_natDegree_succ 📖	mathematical	—	Finset Finset.instHasSubset support Finset.range natDegree	—	supp_subset_range

---

← Back to Index