Laurent

📁 Source: Mathlib/Algebra/Polynomial/Laurent.lean

Statistics

Metric	Count
Definitions LaurentPolynomial, C, T, algebraPolynomial, degree, eval₂, instModulePolynomial, invert, invertibleT, leval, smeval, trunc, «term_[T;T⁻¹]», toLaurent, toLaurentAlg	15
Theorems C_apply, C_eq_algebraMap, T_add, T_apply, T_mul, T_pow, T_sub, T_zero, algebraMap_X_pow, algebraMap_apply, algebraMap_eq_toLaurent, commute_T, degree_C, degree_C_ite, degree_C_le, degree_C_mul_T, degree_C_mul_T_ite, degree_C_mul_T_le, degree_T, degree_T_le, degree_eq_bot_iff, degree_zero, eval₂_C, eval₂_C_mul_T, eval₂_C_mul_T_n, eval₂_C_mul_T_neg_n, eval₂_T, eval₂_T_n, eval₂_T_neg_n, eval₂_toLaurent, exists_T_pow, ext, ext_iff, induction_on, induction_on', induction_on_mul_T, instIsScalarTowerPolynomial, invOf_T, invert_C, invert_T, invert_apply, invert_comp_C, invert_symm, involutive_invert, isLocalization, isUnit_T, leftInverse_trunc_toLaurent, leval_apply, mk'_eq, mk'_mul_T, mk'_one_X, mk'_one_X_pow, mul_T_assoc, reduce_to_polynomial_of_mul_T, single_eq_C, single_eq_C_mul_T, single_zero_one_eq_one, smeval_C, smeval_C_mul, smeval_C_mul_T_n, smeval_T_pow, smeval_add, smeval_congr, smeval_eq_sum, smeval_one, smeval_single, smeval_zero, smul_eq_C_mul, support_C_mul_T, support_C_mul_T_of_ne_zero, toLaurent_reverse, toLaurent_support, trunc_C_mul_T, coe_toLaurentAlg, toLaurentAlg_apply, toLaurent_C, toLaurent_C_mul_T, toLaurent_C_mul_X_pow, toLaurent_C_mul_eq, toLaurent_X, toLaurent_X_pow, toLaurent_apply, toLaurent_comp_C, toLaurent_eq_zero, toLaurent_inj, toLaurent_injective, toLaurent_ne_zero, toLaurent_one, trunc_toLaurent	89
Total	104

LaurentPolynomial

Definitions

Name	Category	Theorems
C 📖	CompOp	36 math math: degree_C_mul_T_ite, eval₂_C_mul_T, Polynomial.toLaurent_C_mul_T, algebraMap_apply, smeval_C_mul, degree_C_mul_T, smeval_C, degree_C, C_apply, Polynomial.toLaurent_comp_C, single_eq_C, eval₂_C_mul_T_neg_n, C_eq_algebraMap, single_eq_C_mul_T, comul_C, eval₂_C, counit_C_mul_T, degree_C_ite, antipode_C, support_C_mul_T_of_ne_zero, counit_C, comul_C_mul_T, smeval_C_mul_T_n, smul_eq_C_mul, Polynomial.toLaurent_C_mul_eq, trunc_C_mul_T, support_C_mul_T, Polynomial.toLaurent_C, Polynomial.toLaurent_C_mul_X_pow, eval₂_C_mul_T_n, comul_C_mul_T_self, invert_C, invert_comp_C, antipode_C_mul_T, degree_C_le, degree_C_mul_T_le
T 📖	CompOp	46 math math: degree_C_mul_T_ite, mk'_one_X_pow, mk'_mul_T, mul_T_assoc, comul_T, commute_T, T_sub, mk'_one_X, smeval_T_pow, T_pow, eval₂_C_mul_T, Polynomial.toLaurent_C_mul_T, invOf_T, antipode_T, degree_C_mul_T, T_zero, eval₂_T, T_apply, mk'_eq, algebraMap_X_pow, Polynomial.toLaurent_X_pow, isUnit_T, eval₂_C_mul_T_neg_n, single_eq_C_mul_T, counit_C_mul_T, eval₂_T_neg_n, support_C_mul_T_of_ne_zero, counit_T, comul_C_mul_T, smeval_C_mul_T_n, eval₂_T_n, trunc_C_mul_T, support_C_mul_T, Polynomial.toLaurent_X, Polynomial.toLaurent_C_mul_X_pow, eval₂_C_mul_T_n, toLaurent_reverse, degree_T_le, comul_C_mul_T_self, T_add, exists_T_pow, antipode_C_mul_T, degree_T, degree_C_mul_T_le, invert_T, T_mul
algebraPolynomial 📖	CompOp	7 math math: mk'_one_X_pow, mk'_mul_T, mk'_one_X, mk'_eq, algebraMap_X_pow, algebraMap_eq_toLaurent, isLocalization
degree 📖	CompOp	10 math math: degree_C_mul_T_ite, degree_C_mul_T, degree_C, degree_C_ite, degree_eq_bot_iff, degree_T_le, degree_zero, degree_C_le, degree_T, degree_C_mul_T_le
eval₂ 📖	CompOp	8 math math: eval₂_C_mul_T, eval₂_T, eval₂_C_mul_T_neg_n, eval₂_C, eval₂_toLaurent, eval₂_T_neg_n, eval₂_T_n, eval₂_C_mul_T_n
instModulePolynomial 📖	CompOp	1 math math: instIsScalarTowerPolynomial
invert 📖	CompOp	7 math math: invert_symm, invert_apply, toLaurent_reverse, invert_C, invert_comp_C, invert_T, involutive_invert
invertibleT 📖	CompOp	1 math math: invOf_T
leval 📖	CompOp	1 math math: leval_apply
smeval 📖	CompOp	11 math math: smeval_eq_sum, smeval_T_pow, smeval_C_mul, smeval_C, leval_apply, smeval_single, smeval_one, smeval_C_mul_T_n, smeval_zero, smeval_add, smeval_congr
trunc 📖	CompOp	3 math math: Polynomial.trunc_toLaurent, leftInverse_trunc_toLaurent, trunc_C_mul_T
«term_[T;T⁻¹]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike RingHom LaurentPolynomial AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C	—	single_eq_C Finsupp.single_apply
C_eq_algebraMap 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C AddMonoidAlgebra.semiring algebraMap AddMonoidAlgebra.algebra Algebra.id	—	—
T_add 📖	mathematical	—	T LaurentPolynomial AddMonoidAlgebra.instMul	—	AddMonoidAlgebra.single_mul_single mul_one
T_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike T AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finsupp.single_apply
T_mul 📖	mathematical	—	LaurentPolynomial AddMonoidAlgebra.instMul T	—	Commute.eq commute_T
T_pow 📖	mathematical	—	LaurentPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Int.instAddMonoid T	—	T.eq_1 AddMonoidAlgebra.single_pow one_pow nsmul_eq_mul
T_sub 📖	mathematical	—	T LaurentPolynomial AddMonoidAlgebra.instMul	—	T_add sub_eq_add_neg
T_zero 📖	mathematical	—	T LaurentPolynomial AddMonoidAlgebra.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
algebraMap_X_pow 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring LaurentPolynomial Semiring.toNonAssocSemiring Polynomial.commSemiring AddMonoidAlgebra.semiring Int.instAddMonoid RingHom.instFunLike algebraMap algebraPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X T	—	Polynomial.toLaurent_X_pow
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.semiring Int.instAddMonoid RingHom.instFunLike algebraMap AddMonoidAlgebra.algebra AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass C	—	—
algebraMap_eq_toLaurent 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring LaurentPolynomial Semiring.toNonAssocSemiring Polynomial.commSemiring AddMonoidAlgebra.semiring Int.instAddMonoid RingHom.instFunLike algebraMap algebraPolynomial Polynomial.semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Polynomial.toLaurent	—	—
commute_T 📖	mathematical	—	Commute LaurentPolynomial AddMonoidAlgebra.instMul T	—	induction_on' Commute.add_right T.eq_1 single_eq_C AddMonoidAlgebra.single_mul_single add_comm add_zero mul_one one_mul single_eq_C_mul_T
degree_C 📖	mathematical	—	degree DFunLike.coe RingHom LaurentPolynomial Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C WithBot WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	mul_one T_zero degree_C_mul_T
degree_C_ite 📖	mathematical	—	degree DFunLike.coe RingHom LaurentPolynomial Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C WithBot MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Bot.bot WithBot.bot WithBot.zero NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass degree_C
degree_C_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt degree DFunLike.coe RingHom LaurentPolynomial Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	LE.le.trans le_of_eq T_zero mul_one degree_C_mul_T_le
degree_C_mul_T 📖	mathematical	—	degree LaurentPolynomial AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T WithBot.some	—	degree.eq_1 support_C_mul_T_of_ne_zero Finset.max_singleton
degree_C_mul_T_ite 📖	mathematical	—	degree LaurentPolynomial AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T WithBot MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Bot.bot WithBot.bot WithBot.some	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul degree_C_mul_T
degree_C_mul_T_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt degree LaurentPolynomial AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T WithBot.some	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul Eq.le degree_C_mul_T
degree_T 📖	mathematical	—	degree T WithBot.some	—	one_mul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass degree_C_mul_T one_ne_zero NeZero.one
degree_T_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt degree T WithBot.some	—	LE.le.trans le_of_eq map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul degree_C_mul_T_le
degree_eq_bot_iff 📖	mathematical	—	degree Bot.bot WithBot WithBot.bot LaurentPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring	—	ext degree_zero
degree_zero 📖	mathematical	—	degree LaurentPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Bot.bot WithBot WithBot.bot	—	—
eval₂_C 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂ C	—	Polynomial.toLaurent_C eval₂_toLaurent Polynomial.eval₂_C
eval₂_C_mul_T 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂ AddMonoidAlgebra.instMul C T Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units DivInvMonoid.toZPow Units.instDivInvMonoid	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass eval₂_C eval₂_T
eval₂_C_mul_T_n 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂ AddMonoidAlgebra.instMul C T Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.val	—	Polynomial.toLaurent_C_mul_T eval₂_toLaurent Polynomial.eval₂_monomial
eval₂_C_mul_T_neg_n 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂ AddMonoidAlgebra.instMul C T Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.val Units Units.instInv	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass eval₂_T_neg_n eval₂_C
eval₂_T 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂ T Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units DivInvMonoid.toZPow Units.instDivInvMonoid	—	CanLift.prf instCanLiftIntNatCastLeOfNat eval₂_T_n LT.lt.le eval₂_T_neg_n zpow_neg zpow_natCast inv_pow Units.val_pow_eq_pow_val
eval₂_T_n 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂ T Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.val	—	Polynomial.toLaurent_X_pow eval₂_toLaurent Polynomial.eval₂_X_pow
eval₂_T_neg_n 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂ T Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.val Units Units.instInv	—	isLocalization mk'_one_X_pow IsLocalization.lift_mk'_spec map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.coe_eval₂RingHom Polynomial.eval₂_X_pow mul_pow Units.mul_inv one_pow
eval₂_toLaurent 📖	mathematical	—	DFunLike.coe RingHom LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂ Polynomial Polynomial.semiring Polynomial.toLaurent Polynomial.eval₂ Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	isLocalization algebraMap_eq_toLaurent IsLocalization.lift_eq Polynomial.coe_eval₂RingHom
exists_T_pow 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring Polynomial.semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike Polynomial.toLaurent AddMonoidAlgebra.instMul T	—	induction_on' map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Polynomial.toLaurent_X_pow mul_T_assoc add_comm add_mul Distrib.rightDistribClass Polynomial.toLaurent_C_mul_eq CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero mul_one Polynomial.toLaurent_C neg_add_cancel
ext 📖	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike	—	—	Finsupp.ext
ext_iff 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike	—	ext
induction_on 📖	—	DFunLike.coe RingHom LaurentPolynomial Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring AddMonoidAlgebra.instMul T	—	—	Int.induction_on mul_one Finset.induction map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.sum_insert ext Finset.sum_congr Finset.sum_apply' Finset.sum_eq_single Finsupp.single_eq_of_ne' Finsupp.single_eq_same Finsupp.notMem_support_iff
induction_on' 📖	—	LaurentPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T	—	—	induction_on mul_one
induction_on_mul_T 📖	—	LaurentPolynomial AddMonoidAlgebra.instMul DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring Polynomial.semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike Polynomial.toLaurent T	—	—	exists_T_pow mul_one T_zero Nat.cast_zero Nat.cast_sub Eq.le T_sub mul_assoc
instIsScalarTowerPolynomial 📖	mathematical	—	IsScalarTower Polynomial LaurentPolynomial SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Polynomial.semiring DistribSMul.toSMulZeroClass instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Int.instAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoidAlgebra.addAddCommMonoid instModulePolynomial	—	smul_eq_mul SemigroupAction.mul_smul
invOf_T 📖	mathematical	—	Invertible.invOf LaurentPolynomial AddMonoidAlgebra.instMul AddMonoidAlgebra.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing T invertibleT	—	—
invert_C 📖	mathematical	—	DFunLike.coe AlgEquiv LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Int.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike invert RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass RingHom.instFunLike C	—	ext invert_apply C_apply
invert_T 📖	mathematical	—	DFunLike.coe AlgEquiv LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Int.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike invert T	—	AddMonoidAlgebra.domCongr_single
invert_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike AlgEquiv LaurentPolynomial AddMonoidAlgebra.semiring Int.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike invert	—	AddMonoidAlgebra.domCongr_apply
invert_comp_C 📖	mathematical	—	LaurentPolynomial CommSemiring.toSemiring DFunLike.coe AlgEquiv AddMonoidAlgebra.semiring Int.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike invert RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass RingHom.instFunLike C	—	ext invert_apply C_apply
invert_symm 📖	mathematical	—	AlgEquiv.symm LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Int.instAddMonoid AddMonoidAlgebra.algebra Algebra.id invert	—	—
involutive_invert 📖	mathematical	—	Function.Involutive LaurentPolynomial CommSemiring.toSemiring DFunLike.coe AlgEquiv AddMonoidAlgebra.semiring Int.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike invert	—	ext invert_apply neg_neg
isLocalization 📖	mathematical	—	IsLocalization.Away Polynomial CommSemiring.toSemiring Polynomial.commSemiring Polynomial.X LaurentPolynomial AddMonoidAlgebra.commSemiring Int.instAddCommMonoid algebraPolynomial	—	algebraMap_eq_toLaurent Polynomial.toLaurent_X_pow isUnit_T induction_on_mul_T mul_T_assoc neg_add_cancel mul_one
isUnit_T 📖	mathematical	—	IsUnit LaurentPolynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Int.instAddMonoid T	—	isUnit_of_invertible
leftInverse_trunc_toLaurent 📖	mathematical	—	Polynomial LaurentPolynomial DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidAlgebra.nonAssocSemiring Int.instAddMonoid Semiring.toNonAssocSemiring Polynomial.semiring AddMonoidHom.instFunLike trunc RingHom RingHom.instFunLike Polynomial.toLaurent	—	Polynomial.induction_on' map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass AddMonoidHom.instAddMonoidHomClass Polynomial.toLaurent_C_mul_T trunc_C_mul_T
leval_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LaurentPolynomial AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module Semiring.toModule LinearMap.instFunLike leval smeval MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Module.toMulActionWithZero	—	—
mk'_eq 📖	mathematical	—	IsLocalization.mk' Polynomial CommSemiring.toSemiring Polynomial.commSemiring Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X LaurentPolynomial AddMonoidAlgebra.commSemiring Int.instAddCommMonoid algebraPolynomial isLocalization Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Monoid.toNatPow AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike Polynomial.toLaurent T	—	isLocalization isUnit_T mul_T_assoc neg_add_cancel T_zero mul_one mk'_mul_T
mk'_mul_T 📖	mathematical	—	LaurentPolynomial CommSemiring.toSemiring AddMonoidAlgebra.instMul IsLocalization.mk' Polynomial Polynomial.commSemiring Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X AddMonoidAlgebra.commSemiring Int.instAddCommMonoid algebraPolynomial isLocalization Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Monoid.toNatPow T DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike Polynomial.toLaurent	—	isLocalization Polynomial.toLaurent_X_pow algebraMap_eq_toLaurent IsLocalization.mk'_spec
mk'_one_X 📖	mathematical	—	IsLocalization.mk' Polynomial CommSemiring.toSemiring Polynomial.commSemiring Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X LaurentPolynomial AddMonoidAlgebra.commSemiring Int.instAddCommMonoid algebraPolynomial isLocalization Polynomial.instOne Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike pow_one T	—	isLocalization pow_one mk'_one_X_pow
mk'_one_X_pow 📖	mathematical	—	IsLocalization.mk' Polynomial CommSemiring.toSemiring Polynomial.commSemiring Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X LaurentPolynomial AddMonoidAlgebra.commSemiring Int.instAddCommMonoid algebraPolynomial isLocalization Polynomial.instOne Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Monoid.toNatPow T	—	isLocalization mk'_eq Polynomial.toLaurent_one one_mul
mul_T_assoc 📖	mathematical	—	LaurentPolynomial AddMonoidAlgebra.instMul T	—	mul_assoc
reduce_to_polynomial_of_mul_T 📖	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring Polynomial.semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike Polynomial.toLaurent	—	—	induction_on_mul_T Nat.cast_zero neg_zero mul_one Nat.cast_add Nat.cast_one neg_add_rev mul_T_assoc neg_add_cancel_comm
single_eq_C 📖	mathematical	—	AddMonoidAlgebra.single DFunLike.coe RingHom LaurentPolynomial Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C	—	—
single_eq_C_mul_T 📖	mathematical	—	AddMonoidAlgebra.single LaurentPolynomial AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T	—	AddMonoidAlgebra.single_mul_single zero_add mul_one
single_zero_one_eq_one 📖	mathematical	—	AddMonoidAlgebra.single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring LaurentPolynomial AddMonoidAlgebra.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
smeval_C 📖	mathematical	—	smeval DFunLike.coe RingHom LaurentPolynomial Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	single_eq_C smeval_single zpow_zero Units.val_one
smeval_C_mul 📖	mathematical	—	smeval MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Module.toMulActionWithZero LaurentPolynomial AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Int.instAddMonoid RingHom.instFunLike C SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction	—	induction_on' mul_add Distrib.leftDistribClass smeval_add smul_add mul_assoc map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass smeval_C_mul_T_n SemigroupAction.mul_smul
smeval_C_mul_T_n 📖	mathematical	—	smeval LaurentPolynomial AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Units.val Units DivInvMonoid.toZPow Units.instDivInvMonoid	—	single_eq_C_mul_T smeval_single
smeval_T_pow 📖	mathematical	—	smeval MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid T Units.val Units DivInvMonoid.toZPow Units.instDivInvMonoid	—	T.eq_1 smeval_single one_smul
smeval_add 📖	mathematical	—	smeval MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Module.toMulActionWithZero LaurentPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Finsupp.sum_add_index zero_smul add_smul
smeval_congr 📖	mathematical	—	smeval	—	—
smeval_eq_sum 📖	mathematical	—	smeval Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass Units.val Units DivInvMonoid.toZPow Units.instDivInvMonoid	—	—
smeval_one 📖	mathematical	—	smeval MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LaurentPolynomial AddMonoidAlgebra.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	T_zero smeval_T_pow zpow_zero Units.val_eq_one
smeval_single 📖	mathematical	—	smeval AddMonoidAlgebra.single SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Units.val Units DivInvMonoid.toZPow Units.instDivInvMonoid	—	Finsupp.sum_single_index zero_smul
smeval_zero 📖	mathematical	—	smeval LaurentPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
smul_eq_C_mul 📖	mathematical	—	LaurentPolynomial SMulZeroClass.toSMul AddZero.toZero AddMonoidAlgebra AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.smulZeroClass DistribSMul.toSMulZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.instMul DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Int.instAddMonoid RingHom.instFunLike C	—	induction_on' smul_add mul_add Distrib.leftDistribClass mul_assoc smul_mul_assoc AddMonoidAlgebra.isScalarTower_self IsScalarTower.left mul_left_inj_of_invertible map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass single_eq_C Finsupp.smul_single'
support_C_mul_T 📖	mathematical	—	Finset Finset.instHasSubset Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LaurentPolynomial Finsupp AddMonoidAlgebra.instMul DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T Finset.instSingleton	—	single_eq_C_mul_T Finsupp.support_single_subset
support_C_mul_T_of_ne_zero 📖	mathematical	—	Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LaurentPolynomial Finsupp AddMonoidAlgebra.instMul DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike C T Finset Finset.instSingleton	—	single_eq_C_mul_T Finsupp.support_single_ne_zero
toLaurent_reverse 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring LaurentPolynomial Semiring.toNonAssocSemiring Polynomial.semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike Polynomial.toLaurent Polynomial.reverse AddMonoidAlgebra.instMul AlgEquiv AddMonoidAlgebra.semiring AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike invert T Polynomial.natDegree	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.natDegree_of_subsingleton CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero mul_one Unique.instSubsingleton map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Polynomial.reverse_add_C map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass Polynomial.toLaurent_C_mul_eq Polynomial.toLaurent_X_pow Polynomial.toLaurent_C SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass invert_C Polynomial.natDegree_add_C add_mul Distrib.rightDistribClass Polynomial.reverse_mul_X map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Polynomial.toLaurent_X NonUnitalAlgSemiHomClass.toMulHomClass invert_T Polynomial.natDegree_mul_X Nat.cast_add Nat.cast_one mul_T_assoc neg_add_cancel_comm_assoc
toLaurent_support 📖	mathematical	—	Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom Polynomial LaurentPolynomial Polynomial.semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike Polynomial.toLaurent Finset.map Nat.castEmbedding AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing Int.instCharZero Polynomial.support	—	Finset.induction_on Int.instCharZero Finset.map_empty Finsupp.support_eq_empty Polynomial.toLaurent_eq_zero Polynomial.support_eq_empty Polynomial.support_erase Finset.erase_insert_eq_erase Finset.erase_eq_of_notMem Polynomial.monomial_add_erase Finset.map_insert map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.toLaurent_C_mul_T Finsupp.support_add_eq Disjoint.mono_left support_C_mul_T Finset.insert_eq support_C_mul_T_of_ne_zero Polynomial.mem_support_iff
trunc_C_mul_T 📖	mathematical	—	DFunLike.coe AddMonoidHom LaurentPolynomial Polynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidAlgebra.nonAssocSemiring Int.instAddMonoid Semiring.toNonAssocSemiring Polynomial.semiring AddMonoidHom.instFunLike trunc AddMonoidAlgebra.instMul RingHom RingHom.instFunLike C T LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Polynomial.module LinearMap.instFunLike Polynomial.monomial Polynomial.instZero	—	RingEquiv.injective RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.apply_symm_apply Int.ofNat_injective Finsupp.comapDomain.addMonoidHom_apply Polynomial.toFinsupp_monomial CanLift.prf instCanLiftIntNatCastLeOfNat Finsupp.comapDomain_single Polynomial.ext Polynomial.coeff_ofFinsupp Finsupp.single_eq_of_ne

Polynomial

Definitions

Name	Category	Theorems
toLaurent 📖	CompOp	23 math math: toLaurent_eq_zero, LaurentPolynomial.mk'_mul_T, trunc_toLaurent, toLaurent_C_mul_T, toLaurent_injective, toLaurent_comp_C, LaurentPolynomial.mk'_eq, toLaurent_apply, LaurentPolynomial.algebraMap_eq_toLaurent, toLaurent_X_pow, LaurentPolynomial.eval₂_toLaurent, LaurentPolynomial.toLaurent_support, toLaurent_inj, toLaurent_one, LaurentPolynomial.leftInverse_trunc_toLaurent, toLaurent_C_mul_eq, toLaurent_X, coe_toLaurentAlg, toLaurent_C, toLaurentAlg_apply, toLaurent_C_mul_X_pow, LaurentPolynomial.toLaurent_reverse, LaurentPolynomial.exists_T_pow
toLaurentAlg 📖	CompOp	2 math math: coe_toLaurentAlg, toLaurentAlg_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toLaurentAlg 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring LaurentPolynomial semiring AddMonoidAlgebra.semiring Int.instAddMonoid algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgHom.funLike toLaurentAlg RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass RingHom.instFunLike toLaurent	—	—
toLaurentAlg_apply 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring LaurentPolynomial semiring AddMonoidAlgebra.semiring Int.instAddMonoid algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgHom.funLike toLaurentAlg RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass RingHom.instFunLike toLaurent	—	—
toLaurent_C 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent C LaurentPolynomial.C	—	mul_one toLaurent_C_mul_T
toLaurent_C_mul_T 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidAlgebra.instMul LaurentPolynomial.C LaurentPolynomial.T	—	toFinsupp_monomial Finsupp.mapDomain_single eq_natCast RingHom.instRingHomClass LaurentPolynomial.single_eq_C_mul_T
toLaurent_C_mul_X_pow 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent instMul C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X AddMonoidAlgebra.instMul LaurentPolynomial.C LaurentPolynomial.T	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass toLaurent_C toLaurent_X_pow
toLaurent_C_mul_eq 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent instMul C AddMonoidAlgebra.instMul LaurentPolynomial.C	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass toLaurent_C
toLaurent_X 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent X LaurentPolynomial.T	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass pow_one one_mul toLaurent_C_mul_T Nat.cast_one
toLaurent_X_pow 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X LaurentPolynomial.T	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass toLaurent_X LaurentPolynomial.T_pow mul_one
toLaurent_apply 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent AddMonoidAlgebra.mapDomain toFinsupp	—	—
toLaurent_comp_C 📖	mathematical	—	Polynomial LaurentPolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent C LaurentPolynomial.C	—	toLaurent_C
toLaurent_eq_zero 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring instZero	—	map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass toLaurent_injective
toLaurent_inj 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent	—	toLaurent_injective
toLaurent_injective 📖	mathematical	—	Polynomial LaurentPolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent	—	LaurentPolynomial.leftInverse_trunc_toLaurent
toLaurent_ne_zero 📖	—	—	—	—	map_ne_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass toLaurent_injective
toLaurent_one 📖	mathematical	—	DFunLike.coe RingHom Polynomial LaurentPolynomial Semiring.toNonAssocSemiring semiring AddMonoidAlgebra.nonAssocSemiring AddMonoid.toAddZeroClass Int.instAddMonoid RingHom.instFunLike toLaurent instOne AddMonoidAlgebra.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
trunc_toLaurent 📖	mathematical	—	DFunLike.coe AddMonoidHom LaurentPolynomial Polynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidAlgebra.nonAssocSemiring Int.instAddMonoid Semiring.toNonAssocSemiring semiring AddMonoidHom.instFunLike LaurentPolynomial.trunc RingHom RingHom.instFunLike toLaurent	—	LaurentPolynomial.leftInverse_trunc_toLaurent

(root)

Definitions

Name	Category	Theorems
LaurentPolynomial 📖	CompOp	86 math math: LaurentPolynomial.degree_C_mul_T_ite, Polynomial.toLaurent_eq_zero, LaurentPolynomial.mk'_one_X_pow, LaurentPolynomial.mk'_mul_T, LaurentPolynomial.mul_T_assoc, LaurentPolynomial.comul_T, LaurentPolynomial.commute_T, LaurentPolynomial.T_sub, LaurentPolynomial.mk'_one_X, LaurentPolynomial.T_pow, Polynomial.trunc_toLaurent, LaurentPolynomial.eval₂_C_mul_T, Polynomial.toLaurent_C_mul_T, LaurentPolynomial.invOf_T, LaurentPolynomial.algebraMap_apply, LaurentPolynomial.antipode_T, LaurentPolynomial.smeval_C_mul, Polynomial.toLaurent_injective, LaurentPolynomial.degree_C_mul_T, LaurentPolynomial.T_zero, LaurentPolynomial.smeval_C, LaurentPolynomial.degree_C, LaurentPolynomial.eval₂_T, LaurentPolynomial.C_apply, Polynomial.toLaurent_comp_C, LaurentPolynomial.mk'_eq, Polynomial.toLaurent_apply, LaurentPolynomial.algebraMap_X_pow, LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow, LaurentPolynomial.leval_apply, LaurentPolynomial.single_eq_C, LaurentPolynomial.isUnit_T, LaurentPolynomial.eval₂_C_mul_T_neg_n, LaurentPolynomial.C_eq_algebraMap, LaurentPolynomial.single_eq_C_mul_T, LaurentPolynomial.comul_C, LaurentPolynomial.eval₂_C, LaurentPolynomial.eval₂_toLaurent, LaurentPolynomial.invert_symm, LaurentPolynomial.toLaurent_support, Polynomial.toLaurent_inj, LaurentPolynomial.invert_apply, LaurentPolynomial.counit_C_mul_T, Polynomial.toLaurent_one, LaurentPolynomial.degree_C_ite, LaurentPolynomial.eval₂_T_neg_n, LaurentPolynomial.smeval_one, LaurentPolynomial.single_zero_one_eq_one, LaurentPolynomial.antipode_C, LaurentPolynomial.instIsCocomm, LaurentPolynomial.support_C_mul_T_of_ne_zero, LaurentPolynomial.counit_T, LaurentPolynomial.counit_C, LaurentPolynomial.comul_C_mul_T, LaurentPolynomial.smeval_C_mul_T_n, LaurentPolynomial.leftInverse_trunc_toLaurent, LaurentPolynomial.smul_eq_C_mul, LaurentPolynomial.degree_eq_bot_iff, Polynomial.toLaurent_C_mul_eq, LaurentPolynomial.eval₂_T_n, LaurentPolynomial.trunc_C_mul_T, LaurentPolynomial.support_C_mul_T, Polynomial.toLaurent_X, LaurentPolynomial.isLocalization, Polynomial.coe_toLaurentAlg, LaurentPolynomial.smeval_zero, Polynomial.toLaurent_C, Polynomial.toLaurentAlg_apply, Polynomial.toLaurent_C_mul_X_pow, LaurentPolynomial.eval₂_C_mul_T_n, LaurentPolynomial.toLaurent_reverse, LaurentPolynomial.smeval_add, LaurentPolynomial.comul_C_mul_T_self, LaurentPolynomial.instIsScalarTowerPolynomial, LaurentPolynomial.invert_C, LaurentPolynomial.T_add, LaurentPolynomial.exists_T_pow, LaurentPolynomial.degree_zero, LaurentPolynomial.invert_comp_C, LaurentPolynomial.antipode_C_mul_T, LaurentPolynomial.degree_C_le, LaurentPolynomial.degree_C_mul_T_le, LaurentPolynomial.invert_T, LaurentPolynomial.T_mul, LaurentPolynomial.involutive_invert

---

← Back to Index