Trunc

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

Statistics

Metric	Count
Definitions trunc, trunc', truncFun, truncFun'	4
Theorems coeff_mul_eq_coeff_trunc'_mul_trunc', coeff_trunc, coeff_trunc', coeff_truncFun, coeff_truncFun', eq_iff_frequently_trunc'_eq, ext_trunc', totalDegree_trunc', trunc'_C, trunc'_C_mul, trunc'_map, trunc'_one, trunc'_trunc', trunc'_trunc'_pow, trunc_C, trunc_C_mul, trunc_map, trunc_one	18
Total	22

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	14 math math: eq_iff_frequently_trunc'_eq, trunc'_trunc', trunc'_expand_trunc', ext_trunc', trunc'_trunc'_pow, 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
truncFun 📖	CompOp	1 math math: coeff_truncFun
truncFun' 📖	CompOp	1 math math: coeff_truncFun'

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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MvPolynomial.commSemiring AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidHom.instFunLike trunc'	—	coeff_mul MvPolynomial.coeff_mul Finset.sum_congr Nat.instCanonicallyOrderedAdd coeff_trunc' le_trans le_self_add Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_add_self
coeff_trunc 📖	mathematical	—	MvPolynomial.coeff DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc Finsupp MulZeroClass.toZero Nat.instMulZeroClass Preorder.toLT Finsupp.preorder Nat.instPreorder Finsupp.decidableLT Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd LinearMap RingHom.id instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd coeff_truncFun
coeff_trunc' 📖	mathematical	—	MvPolynomial.coeff DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc' Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE Finsupp.decidableLE Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd LinearMap RingHom.id instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff NonUnitalNonAssocSemiring.toMulZeroClass	—	coeff_truncFun'
coeff_truncFun 📖	mathematical	—	MvPolynomial.coeff truncFun Finsupp MulZeroClass.toZero Nat.instMulZeroClass Preorder.toLT Finsupp.preorder Nat.instPreorder Finsupp.decidableLT Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd MvPolynomial.coeff_sum Finset.sum_congr MvPolynomial.coeff_monomial Finset.sum_ite_eq'
coeff_truncFun' 📖	mathematical	—	MvPolynomial.coeff truncFun' Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE Finsupp.decidableLE Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd 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 AddMonoidHom MvPowerSeries AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.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 AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc'	—	ext Nat.instCanonicallyOrderedAdd coeff_trunc' le_rfl
totalDegree_trunc' 📖	mathematical	—	MvPolynomial.totalDegree DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc' Finsupp AddZero.toZero AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Finsupp.instAddZeroClass Finsupp.degree	—	Set.toFinset_Icc Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid coeff_trunc' eq_of_le_of_ge Finset.le_sup Finset.sum_congr LE.le.trans Finset.sum_le_sum_of_subset Finsupp.support_mono Finset.sum_le_sum MvPolynomial.totalDegree.eq_1 Finset.sup_mono
trunc'_C 📖	mathematical	—	DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc' RingHom instSemiring RingHom.instFunLike C MvPolynomial.C	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc' coeff_C MvPolynomial.coeff_C zero_le Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
trunc'_C_mul 📖	mathematical	—	DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc' instMul RingHom instSemiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring 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 AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc' RingHom instSemiring RingHom.instFunLike map MvPolynomial.map	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc' MvPolynomial.coeff_map map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
trunc'_one 📖	mathematical	—	DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc' instOne AddMonoidWithOne.toOne	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc' coeff_one MvPolynomial.coeff_zero_one MvPolynomial.coeff_one zero_le Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
trunc'_trunc' 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE	DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc' MvPolynomial.toMvPowerSeries	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc' LE.le.trans
trunc'_trunc'_pow 📖	mathematical	—	DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc' Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring MvPolynomial.toMvPowerSeries	—	Nat.le_induction pow_one trunc'_trunc' MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc' pow_succ coeff_mul_eq_coeff_trunc'_mul_trunc' MvPolynomial.coeff_mul coeff_mul Finset.sum_congr LE.le.trans self_le_add_right Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finset.HasAntidiagonal.mem_antidiagonal self_le_add_left
trunc_C 📖	mathematical	—	DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc RingHom instSemiring RingHom.instFunLike C MvPolynomial.C	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc coeff_C MvPolynomial.coeff_C Ne.bot_lt
trunc_C_mul 📖	mathematical	—	DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc instMul RingHom instSemiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring 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 AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc RingHom instSemiring RingHom.instFunLike map MvPolynomial.map	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc MvPolynomial.coeff_map map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
trunc_one 📖	mathematical	—	DFunLike.coe AddMonoidHom MvPowerSeries MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.instFunLike trunc instOne AddMonoidWithOne.toOne	—	MvPolynomial.ext Nat.instCanonicallyOrderedAdd coeff_trunc coeff_one MvPolynomial.coeff_zero_one MvPolynomial.coeff_one Ne.bot_lt

---

← Back to Index