Trunc

📁 Source: Mathlib/RingTheory/MvPowerSeries/Trunc.lean

Statistics

Metric	Count
Definitions trunc, trunc', truncFinset	3
Theorems coeff_mul_eq_coeff_trunc'_mul_trunc', coeff_trunc, coeff_trunc', coeff_trunc'_mul_trunc'_eq_coeff_mul, coeff_truncFinset, coeff_truncFinset_eq_zero, coeff_truncFinset_mul_truncFinset_eq_coeff_mul, coeff_truncFinset_of_mem, eq_iff_frequently_trunc'_eq, ext_trunc', support_truncFinset_subset, totalDegree_trunc', totalDegree_truncFinset, trunc'_C, trunc'_C_mul, trunc'_map, trunc'_one, trunc'_trunc', trunc'_trunc'_pow, truncFinset_C, truncFinset_apply, truncFinset_map, truncFinset_monomial, truncFinset_monomial_eq_zero, truncFinset_one, truncFinset_truncFinset, truncFinset_truncFinset_pow, trunc_C, trunc_C_mul, trunc_map, trunc_one	31
Total	34

MvPowerSeries

Definitions

Name	Category	Theorems
trunc 📖	CompOp	6 math math: WithPiTopology.tendsto_trunc_atTop, trunc_C, trunc_one, trunc_map, coeff_trunc, trunc_C_mul
trunc' 📖	CompOp	15 math math: eq_iff_frequently_trunc'_eq, trunc'_trunc', trunc'_expand_trunc', ext_trunc', trunc'_trunc'_pow, coeff_trunc'_mul_trunc'_eq_coeff_mul, trunc'_expand, coeff_trunc', totalDegree_trunc', coeff_mul_eq_coeff_trunc'_mul_trunc', WithPiTopology.tendsto_trunc'_atTop, trunc'_one, trunc'_map, trunc'_C, trunc'_C_mul
truncFinset 📖	CompOp	14 math math: truncFinset_one, coeff_truncFinset_of_mem, truncFinset_C, truncFinset_map, coeff_truncFinset_mul_truncFinset_eq_coeff_mul, truncFinset_monomial_eq_zero, truncFinset_monomial, totalDegree_truncFinset, coeff_truncFinset_eq_zero, truncFinset_truncFinset, support_truncFinset_subset, coeff_truncFinset, truncFinset_apply, truncFinset_truncFinset_pow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_mul_eq_coeff_trunc'_mul_trunc' 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff instMul MvPolynomial.coeff MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module trunc'	—	coeff_trunc'_mul_trunc'_eq_coeff_mul
coeff_trunc 📖	mathematical	—	MvPolynomial.coeff DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc Preorder.toLT Finsupp.preorder Nat.instPreorder Finsupp.decidableLT Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd coeff NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd coeff_truncFinset
coeff_trunc' 📖	mathematical	—	MvPolynomial.coeff DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' Finsupp.instLE Finsupp.decidableLE Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd coeff NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd coeff_truncFinset
coeff_trunc'_mul_trunc'_eq_coeff_mul 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE	MvPolynomial.coeff MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' coeff instMul	—	coeff_truncFinset_mul_truncFinset_eq_coeff_mul Nat.instCanonicallyOrderedAdd
coeff_truncFinset 📖	mathematical	—	MvPolynomial.coeff DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset Finset SetLike.instMembership Finset.instSetLike Finset.decidableMem Finsupp.instDecidableEq coeff NonUnitalNonAssocSemiring.toMulZeroClass	—	truncFinset_apply MvPolynomial.coeff_sum Finset.sum_congr MvPolynomial.coeff_monomial Finset.sum_ite_eq'
coeff_truncFinset_eq_zero 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike	MvPolynomial.coeff DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset NonUnitalNonAssocSemiring.toMulZeroClass	—	truncFinset_apply MvPolynomial.coeff_sum Finset.sum_congr MvPolynomial.coeff_monomial Finset.sum_ite_eq'
coeff_truncFinset_mul_truncFinset_eq_coeff_mul 📖	mathematical	IsLowerSet Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE SetLike.coe Finset Finset.instSetLike SetLike.instMembership	MvPolynomial.coeff MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset coeff instMul	—	MvPolynomial.coeff_mul coeff_mul Finset.sum_congr coeff_truncFinset_of_mem IsOrderedAddMonoid.toAddLeftMono Finsupp.isOrderedAddMonoid Nat.instIsOrderedAddMonoid Finsupp.addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT Finsupp.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT Finsupp.isOrderedCancelAddMonoid
coeff_truncFinset_of_mem 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike	MvPolynomial.coeff DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset coeff	—	truncFinset_apply MvPolynomial.coeff_sum Finset.sum_congr MvPolynomial.coeff_monomial Finset.sum_ite_eq'
eq_iff_frequently_trunc'_eq 📖	mathematical	—	Filter.Frequently Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' Filter.atTop Finsupp.preorder Nat.instPreorder	—	SemilatticeSup.instIsDirectedOrder ext Filter.Frequently.forall_exists_of_atTop Nat.instCanonicallyOrderedAdd coeff_trunc'
ext_trunc' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc'	—	ext Nat.instCanonicallyOrderedAdd coeff_trunc' le_rfl
support_truncFinset_subset 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset MvPolynomial.support DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset	—	Mathlib.Tactic.Contrapose.contrapose₁ coeff_truncFinset_eq_zero
totalDegree_trunc' 📖	mathematical	—	MvPolynomial.totalDegree DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' AddMonoidHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Finsupp.instAddZeroClass AddMonoidHom.instFunLike Finsupp.degree	—	Nat.instCanonicallyOrderedAdd Finset.sup_Iic_of_monotone Finsupp.degree_mono totalDegree_truncFinset
totalDegree_truncFinset 📖	mathematical	—	MvPolynomial.totalDegree DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset Finset.sup Lattice.toSemilatticeSup Nat.instLattice Nat.instOrderBot AddMonoidHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Finsupp.instAddZeroClass AddMonoidHom.instFunLike Finsupp.degree	—	Finset.sup_mono support_truncFinset_subset
trunc'_C 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' RingHom instSemiring RingHom.instFunLike C AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial.C	—	truncFinset_C Nat.instCanonicallyOrderedAdd Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
trunc'_C_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' instMul RingHom instSemiring RingHom.instFunLike C AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass MvPolynomial.C	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc' coeff_C_mul MvPolynomial.coeff_C_mul mul_ite MulZeroClass.mul_zero
trunc'_map 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' RingHom instSemiring RingHom.instFunLike map AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial.map	—	truncFinset_map Nat.instCanonicallyOrderedAdd
trunc'_one 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' instOne AddMonoidAlgebra.zero Finsupp.instZero	—	truncFinset_one Nat.instCanonicallyOrderedAdd Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
trunc'_trunc' 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' MvPolynomial.toMvPowerSeries	—	truncFinset_truncFinset Nat.instCanonicallyOrderedAdd Finset.Iic_subset_Iic
trunc'_trunc'_pow 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc' Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring MvPolynomial.toMvPowerSeries	—	truncFinset_truncFinset_pow Nat.instCanonicallyOrderedAdd
truncFinset_C 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike Finsupp.instZero	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset RingHom instSemiring RingHom.instFunLike C AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial.C	—	truncFinset_monomial
truncFinset_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset Finset.sum MvPolynomial.monomial coeff	—	—
truncFinset_map 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset RingHom instSemiring RingHom.instFunLike map AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial.map	—	MvPolynomial.ext
truncFinset_monomial 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset monomial MvPolynomial.monomial	—	MvPolynomial.ext
truncFinset_monomial_eq_zero 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset monomial NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	MvPolynomial.ext Finset.sum_congr coeff_monomial MvPolynomial.coeff_sum MvPolynomial.coeff_monomial Finset.sum_ite_eq'
truncFinset_one 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike Finsupp.instZero	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset instOne AddMonoidAlgebra.zero Finsupp.instZero	—	truncFinset_C
truncFinset_truncFinset 📖	mathematical	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset MvPolynomial.toMvPowerSeries	—	MvPolynomial.ext
truncFinset_truncFinset_pow 📖	mathematical	IsLowerSet Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE SetLike.coe Finset Finset.instSetLike	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike truncFinset Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring MvPolynomial.toMvPowerSeries	—	Nat.le_induction pow_one truncFinset_truncFinset Finset.instReflSubset MvPolynomial.ext coeff_truncFinset_of_mem pow_succ coeff_truncFinset_mul_truncFinset_eq_coeff_mul subset_refl coeff_truncFinset_eq_zero
trunc_C 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc RingHom instSemiring RingHom.instFunLike C AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial.C	—	truncFinset_C Nat.instCanonicallyOrderedAdd pos_of_ne_zero Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
trunc_C_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc instMul RingHom instSemiring RingHom.instFunLike C AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass MvPolynomial.C	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc coeff_C_mul MvPolynomial.coeff_C_mul mul_ite MulZeroClass.mul_zero
trunc_map 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc RingHom instSemiring RingHom.instFunLike map AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial.map	—	truncFinset_map Nat.instCanonicallyOrderedAdd
trunc_one 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries MvPolynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike trunc instOne AddMonoidAlgebra.zero Finsupp.instZero	—	truncFinset_one Nat.instCanonicallyOrderedAdd pos_of_ne_zero Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid

---

← Back to Index