Trunc

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

Statistics

Metric	Count
Definitions trunc, Trunc	2
Theorems coeff_coe_trunc_of_lt, coeff_mul_eq_coeff_trunc_mul_trunc, coeff_mul_eq_coeff_trunc_mul_trunc₂, coeff_trunc, degree_trunc_lt, eq_X_pow_mul_shift_add_trunc, eq_shift_mul_X_pow_add_trunc, eval₂_trunc_eq_sum_range, monomial_eq_C_mul_X_pow, natDegree_trunc_lt, trunc_C, trunc_C_mul, trunc_X, trunc_X_of, trunc_X_pow_self_mul, trunc_apply, trunc_coe_eq_self, trunc_map, trunc_mul_C, trunc_mul_trunc, trunc_one, trunc_one_X, trunc_one_left, trunc_sub, trunc_succ, trunc_trunc, trunc_trunc_mul, trunc_trunc_mul_trunc, trunc_trunc_of_le, trunc_trunc_pow, trunc_zero'	31
Total	33

PowerSeries

Definitions

Name	Category	Theorems
trunc 📖	CompOp	34 math math: coeff_mul_eq_coeff_trunc_mul_trunc₂, coeff_trunc, trunc_mul_trunc, trunc_X_pow_self_mul, eq_shift_mul_X_pow_add_trunc, degree_trunc_lt, trunc_trunc_mul_trunc, trunc_mul_C, trunc_X_of, trunc_trunc_mul, eq_X_pow_mul_shift_add_trunc, trunc_trunc_of_le, trunc_one_left, trunc_C, trunc_trunc_pow, trunc_apply, trunc_one, trunc_succ, coeff_mul_eq_coeff_trunc_mul_trunc, trunc_coe_eq_self, eval₂_trunc_eq_sum_range, trunc_one_X, trunc_trunc, WithPiTopology.tendsto_trunc_atTop, trunc_sub, trunc_derivativeFun, trunc_map, coeff_coe_trunc_of_lt, trunc_zero', trunc_derivative, natDegree_trunc_lt, trunc_X, trunc_C_mul, trunc_derivative'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_coe_trunc_of_lt 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Polynomial.toPowerSeries Polynomial Polynomial.semiring Polynomial.module trunc	—	Polynomial.coeff_coe coeff_trunc
coeff_mul_eq_coeff_trunc_mul_trunc 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff MvPowerSeries.instMul Polynomial.toPowerSeries Polynomial Polynomial.semiring Polynomial.module trunc	—	coeff_mul_eq_coeff_trunc_mul_trunc₂
coeff_mul_eq_coeff_trunc_mul_trunc₂ 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff MvPowerSeries.instMul Polynomial.toPowerSeries Polynomial Polynomial.semiring Polynomial.module trunc	—	coeff_coe_trunc_of_lt trunc_trunc_mul_trunc trunc_trunc_of_le
coeff_trunc 📖	mathematical	—	Polynomial.coeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
degree_trunc_lt 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne	—	coeff_trunc
eq_X_pow_mul_shift_add_trunc 📖	mathematical	—	PowerSeries Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring MvPowerSeries.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X DFunLike.coe LinearMap RingHom.id instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instModule Semiring.toModule LinearMap.instFunLike coeff Polynomial.toPowerSeries Polynomial Polynomial.semiring Polynomial.module trunc	—	Commute.eq commute_X_pow eq_shift_mul_X_pow_add_trunc
eq_shift_mul_X_pow_add_trunc 📖	mathematical	—	PowerSeries Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring MvPowerSeries.instMul DFunLike.coe LinearMap RingHom.id instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instModule Semiring.toModule LinearMap.instFunLike coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Polynomial.toPowerSeries Polynomial Polynomial.semiring Polynomial.module trunc	—	ext map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Polynomial.coeff_coe coeff_mul_X_pow' coeff_trunc ite_add_ite add_zero zero_add
eval₂_trunc_eq_sum_range 📖	mathematical	—	Polynomial.eval₂ DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Finset.sum Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	trunc_zero' Finset.range_zero Finset.sum_empty Polynomial.eval₂_zero natDegree_trunc_lt Polynomial.eval₂_eq_sum_range' Finset.sum_congr coeff_trunc Finset.mem_range
monomial_eq_C_mul_X_pow 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid Semiring.toModule instModule LinearMap.instFunLike monomial MvPowerSeries.instMul RingHom instSemiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	ext coeff_monomial coeff_C_mul coeff_X_pow mul_ite mul_one MulZeroClass.mul_zero
natDegree_trunc_lt 📖	mathematical	—	Polynomial.natDegree DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc	—	Nat.instNoMaxOrder coeff_trunc
trunc_C 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc RingHom instSemiring RingHom.instFunLike C Polynomial.C	—	Polynomial.ext coeff_trunc coeff_C Polynomial.coeff_C IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd
trunc_C_mul 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc MvPowerSeries.instMul RingHom instSemiring RingHom.instFunLike C Polynomial.instMul Polynomial.C	—	Polynomial.ext coeff_trunc coeff_C_mul Polynomial.coeff_C_mul mul_ite MulZeroClass.mul_zero
trunc_X 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc X Polynomial.X	—	Polynomial.ext coeff_trunc coeff_X Polynomial.coeff_X_one Polynomial.coeff_X_of_ne_one
trunc_X_of 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc X Polynomial.X	—	trunc_X
trunc_X_pow_self_mul 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc MvPowerSeries.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring X Polynomial.instZero	—	Polynomial.ext coeff_trunc coeff_X_pow_mul'
trunc_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Finset.sum Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Polynomial.monomial coeff	—	—
trunc_coe_eq_self 📖	mathematical	Polynomial.natDegree CommSemiring.toSemiring	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Polynomial.toPowerSeries	—	ext Polynomial.coeff_coe coeff_trunc Polynomial.coeff_eq_zero_of_natDegree_lt lt_of_lt_of_le not_lt
trunc_map 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc RingHom instSemiring RingHom.instFunLike map Polynomial.map	—	Polynomial.ext coeff_trunc Polynomial.coeff_map map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
trunc_mul_C 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc MvPowerSeries.instMul RingHom instSemiring RingHom.instFunLike C Polynomial.instMul Polynomial.C	—	Polynomial.ext coeff_trunc coeff_mul_C Polynomial.coeff_mul_C ite_mul MulZeroClass.zero_mul
trunc_mul_trunc 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc MvPowerSeries.instMul Polynomial.toPowerSeries	—	mul_comm trunc_trunc_mul
trunc_one 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc MvPowerSeries.instOne Polynomial.instOne	—	Polynomial.ext
trunc_one_X 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc X Polynomial.instZero	—	trunc_one_left coeff_zero_X map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
trunc_one_left 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc RingHom RingHom.instFunLike Polynomial.C coeff	—	Polynomial.ext coeff_trunc coeff_zero_eq_constantCoeff Polynomial.coeff_C
trunc_sub 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc SubNegMonoid.toSub AddGroup.toSubNegMonoid instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Polynomial.instSub	—	Polynomial.ext map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Polynomial.coeff_sub
trunc_succ 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Polynomial.instAdd Polynomial.monomial coeff	—	trunc_apply Nat.Ico_zero_eq_range Finset.sum_range_succ
trunc_trunc 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Polynomial.toPowerSeries	—	trunc_trunc_of_le le_refl
trunc_trunc_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc MvPowerSeries.instMul Polynomial.toPowerSeries	—	Polynomial.ext coeff_trunc coeff_mul Finset.sum_congr lt_of_le_of_lt Finset.antidiagonal.fst_le Nat.instCanonicallyOrderedAdd Polynomial.coeff_coe
trunc_trunc_mul_trunc 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc MvPowerSeries.instMul Polynomial.toPowerSeries	—	trunc_trunc_mul trunc_mul_trunc
trunc_trunc_of_le 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Polynomial.toPowerSeries	—	Polynomial.ext coeff_trunc Polynomial.coeff_coe lt_of_lt_of_le
trunc_trunc_pow 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Polynomial.toPowerSeries	—	pow_zero pow_succ' trunc_trunc_mul trunc_trunc_mul_trunc
trunc_zero' 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Polynomial.instZero	—	—

(root)

Definitions

Name	Category	Theorems
Trunc 📖	CompOp	4 math math: Trunc.instSubsingletonTrunc, Trunc.instLawfulMonad, Trunc.finChoiceEquiv_symm_apply, Trunc.finChoiceEquiv_apply

---

← Back to Index