WeierstrassPreparation

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

Statistics

Metric	Count
Definitions `algEquivQuotient`, `IsWeierstrassDivision`, `IsWeierstrassDivisionAt`, `IsWeierstrassDivisor`, `IsWeierstrassDivisorAt`, `div`, `divCoeff`, `mod'`, `seq`, `IsWeierstrassFactorization`, `IsWeierstrassFactorizationAt`, `algEquivQuotient`, `algEquivQuotientWeierstrassDistinguished`, `weierstrassDistinguished`, `weierstrassDiv`, `weierstrassMod`, `weierstrassUnit`, `«term_%ʷ_»`, `«term_/ʷ_»`	19
Theorems `algEquivQuotient_apply`, `algEquivQuotient_symm_apply`, `isWeierstrassDivisorAt`, `isWeierstrassDivisorAt'`, `elim`, `eq_zero`, `isUnit_of_map_ne_zero`, `isWeierstrassFactorization`, `unique`, `add`, `coeff_f_sub_r_mem`, `degree_lt`, `eq_mul_add`, `smul`, `of_map_ne_zero`, `coeff_div`, `coeff_div_sub_seq_mem`, `coeff_seq_mem`, `coeff_seq_succ_sub_seq_mem`, `div_add`, `div_coe_eq_zero`, `div_smul`, `div_zero`, `eq_of_mul_add_eq_mul_add`, `eq_zero_of_mul_eq`, `isUnit_shift`, `isWeierstrassDivisionAt_div_mod`, `mk_mod'_eq_self`, `mod'_mk_eq_mod`, `mod_add`, `mod_coe_eq_self`, `mod_smul`, `mod_zero`, `seq_one`, `seq_zero`, `degree_eq_coe_lift_order_map`, `elim`, `isWeierstrassDivision`, `map_ne_zero`, `natDegree_eq_toNat_order_map`, `unique`, `algEquivQuotient_apply`, `algEquivQuotient_symm_apply`, `degree_eq_coe_lift_order_map_of_ne_top`, `eq_mul`, `isDistinguishedAt`, `isUnit`, `map_ne_zero_of_ne_top`, `mul`, `natDegree_eq_toNat_order_map_of_ne_top`, `smul`, `add_weierstrassDiv`, `add_weierstrassMod`, `degree_weierstrassMod_lt`, `eq_mul_weierstrassDiv_add_weierstrassMod`, `eq_weierstrassDistinguished_mul_weierstrassUnit`, `exists_isWeierstrassDivision`, `exists_isWeierstrassFactorization`, `isDistinguishedAt_weierstrassDistinguished`, `isUnit_weierstrassUnit`, `isWeierstrassDivisionAt_iff`, `isWeierstrassDivisionAt_zero`, `isWeierstrassDivision_weierstrassDiv_weierstrassMod`, `isWeierstrassFactorizationAt_iff`, `isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit`, `smul_weierstrassDiv`, `smul_weierstrassMod`, `weierstrassDistinguished_mul`, `weierstrassDistinguished_smul`, `weierstrassDiv_zero`, `weierstrassDiv_zero_left`, `weierstrassDiv_zero_right`, `weierstrassMod_zero`, `weierstrassMod_zero_left`, `weierstrassMod_zero_right`, `weierstrassUnit_mul`, `weierstrassUnit_smul`, `zero_weierstrassDiv`, `zero_weierstrassMod`	79
Total	98

Polynomial.IsDistinguishedAt

Definitions

Name	Category	Theorems
`algEquivQuotient` 📖	CompOp	2 math math: `algEquivQuotient_symm_apply`, `algEquivQuotient_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquivQuotient_apply` 📖	mathematical	`Polynomial.IsDistinguishedAt`	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Polynomial.semiring` `Ideal.instHasQuotient_1` `Polynomial.commRing` `Ideal.span` `Set` `Set.instSingletonSet` `PowerSeries` `PowerSeries.instSemiring` `PowerSeries.instCommRing` `Polynomial.toPowerSeries` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `Polynomial.algebraOfAlgebra` `Algebra.id` `PowerSeries.instAlgebra` `AlgEquiv.instFunLike` `algEquivQuotient` `AlgHom` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `Ideal.instHasQuotient` `PowerSeries.instRing` `Ideal.Quotient.ring` `Ideal.Quotient.algebra` `AlgHom.funLike` `Ideal.quotientMapₐ` `Polynomial.coeToPowerSeries.algHom`	—	—
`algEquivQuotient_symm_apply` 📖	mathematical	`Polynomial.IsDistinguishedAt`	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `PowerSeries` `Ideal` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `PowerSeries.instCommRing` `Ideal.span` `Set` `Set.instSingletonSet` `Polynomial.toPowerSeries` `Polynomial` `Polynomial.semiring` `Polynomial.commRing` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `PowerSeries.instAlgebra` `Algebra.id` `Polynomial.algebraOfAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `algEquivQuotient` `RingHom` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `RingHom.instFunLike` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Submodule.Quotient.module'` `PowerSeries.instRing` `PowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `PowerSeries.instModule` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Polynomial.module` `LinearMap.instFunLike` `PowerSeries.IsWeierstrassDivisorAt.mod'`	—	—
`isWeierstrassDivisorAt` 📖	mathematical	`Polynomial.IsDistinguishedAt`	`PowerSeries.IsWeierstrassDivisorAt` `Polynomial.toPowerSeries` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Ideal.instIsTwoSided_1` `coe_natDegree_eq_order_map` `PowerSeries.constantCoeff_one` `Ideal.ne_top_iff_one` `mul_one` `Polynomial.coeff_coe` `Polynomial.Monic.leadingCoeff` `monic`
`isWeierstrassDivisorAt'` 📖	mathematical	`Polynomial.IsDistinguishedAt`	`PowerSeries.IsWeierstrassDivisorAt` `Polynomial.toPowerSeries` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`eq_or_ne` `IsHausdorff.subsingleton` `isUnit_of_subsingleton` `Ideal.instIsTwoSided_1` `isWeierstrassDivisorAt`

PowerSeries

Definitions

Name	Category	Theorems
`IsWeierstrassDivision` 📖	MathDef	3 math math: `IsWeierstrassFactorization.isWeierstrassDivision`, `isWeierstrassDivision_weierstrassDiv_weierstrassMod`, `exists_isWeierstrassDivision`
`IsWeierstrassDivisionAt` 📖	CompData	3 math math: `isWeierstrassDivisionAt_iff`, `IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod`, `isWeierstrassDivisionAt_zero`
`IsWeierstrassDivisor` 📖	MathDef	1 math math: `IsWeierstrassDivisor.of_map_ne_zero`
`IsWeierstrassDivisorAt` 📖	MathDef	2 math math: `Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt`, `Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt'`
`IsWeierstrassFactorization` 📖	MathDef	3 math math: `isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit`, `exists_isWeierstrassFactorization`, `IsWeierstrassDivision.isWeierstrassFactorization`
`IsWeierstrassFactorizationAt` 📖	CompData	1 math math: `isWeierstrassFactorizationAt_iff`
`algEquivQuotientWeierstrassDistinguished` 📖	CompOp	—
`weierstrassDistinguished` 📖	CompOp	6 math math: `weierstrassDistinguished_mul`, `isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit`, `IsWeierstrassFactorization.unique`, `isDistinguishedAt_weierstrassDistinguished`, `eq_weierstrassDistinguished_mul_weierstrassUnit`, `weierstrassDistinguished_smul`
`weierstrassDiv` 📖	CompOp	9 math math: `zero_weierstrassDiv`, `eq_mul_weierstrassDiv_add_weierstrassMod`, `smul_weierstrassDiv`, `IsWeierstrassDivision.unique`, `isWeierstrassDivision_weierstrassDiv_weierstrassMod`, `weierstrassDiv_zero`, `weierstrassDiv_zero_right`, `weierstrassDiv_zero_left`, `add_weierstrassDiv`
`weierstrassMod` 📖	CompOp	10 math math: `zero_weierstrassMod`, `eq_mul_weierstrassDiv_add_weierstrassMod`, `degree_weierstrassMod_lt`, `IsWeierstrassDivision.unique`, `isWeierstrassDivision_weierstrassDiv_weierstrassMod`, `smul_weierstrassMod`, `weierstrassMod_zero_left`, `add_weierstrassMod`, `weierstrassMod_zero_right`, `weierstrassMod_zero`
`weierstrassUnit` 📖	CompOp	6 math math: `weierstrassUnit_mul`, `isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit`, `isUnit_weierstrassUnit`, `IsWeierstrassFactorization.unique`, `eq_weierstrassDistinguished_mul_weierstrassUnit`, `weierstrassUnit_smul`
`«term_%ʷ_»` 📖	CompOp	—
`«term_/ʷ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_weierstrassDiv` 📖	mathematical	—	`weierstrassDiv` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring`	—	`IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisor.of_map_ne_zero` `IsWeierstrassDivisorAt.div_add` `add_zero`
`add_weierstrassMod` 📖	mathematical	—	`weierstrassMod` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `Polynomial` `Polynomial.instAdd`	—	`IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisor.of_map_ne_zero` `IsWeierstrassDivisorAt.mod_add` `add_zero`
`degree_weierstrassMod_lt` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `weierstrassMod` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.toNat` `order` `IsLocalRing.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `map` `IsLocalRing.residue`	—	`IsWeierstrassDivisor.of_map_ne_zero` `weierstrassMod.eq_1` `degree_trunc_lt` `Ideal.instIsTwoSided_1` `Polynomial.degree_zero` `WithBot.bot_lt_coe`
`eq_mul_weierstrassDiv_add_weierstrassMod` 📖	mathematical	—	`PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `weierstrassDiv` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `Polynomial.toPowerSeries` `weierstrassMod`	—	`IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisor.of_map_ne_zero` `IsWeierstrassDivisionAt.eq_mul_add` `IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod`
`eq_weierstrassDistinguished_mul_weierstrassUnit` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.toPowerSeries` `weierstrassDistinguished` `weierstrassUnit`	—	`IsWeierstrassFactorizationAt.eq_mul` `exists_isWeierstrassFactorization`
`exists_isWeierstrassDivision` 📖	mathematical	—	`IsWeierstrassDivision`	—	`IsWeierstrassDivisor.of_map_ne_zero` `IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod`
`exists_isWeierstrassFactorization` 📖	mathematical	—	`IsWeierstrassFactorization`	—	`exists_isWeierstrassDivision` `IsWeierstrassDivision.isUnit_of_map_ne_zero` `IsWeierstrassDivision.isWeierstrassFactorization`
`isDistinguishedAt_weierstrassDistinguished` 📖	mathematical	—	`Polynomial.IsDistinguishedAt` `weierstrassDistinguished` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring`	—	`IsWeierstrassFactorizationAt.isDistinguishedAt` `exists_isWeierstrassFactorization`
`isUnit_weierstrassUnit` 📖	mathematical	—	`IsUnit` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `weierstrassUnit`	—	`IsWeierstrassFactorizationAt.isUnit` `exists_isWeierstrassFactorization`
`isWeierstrassDivisionAt_iff` 📖	mathematical	—	`IsWeierstrassDivisionAt` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.toNat` `order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `map` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	—	`Ideal.instIsTwoSided_1`
`isWeierstrassDivisionAt_zero` 📖	mathematical	—	`IsWeierstrassDivisionAt` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero`	—	`Ideal.instIsTwoSided_1` `Polynomial.degree_zero` `WithBot.bot_lt_coe` `MulZeroClass.mul_zero` `add_zero`
`isWeierstrassDivision_weierstrassDiv_weierstrassMod` 📖	mathematical	—	`IsWeierstrassDivision` `weierstrassDiv` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `weierstrassMod`	—	`IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisor.of_map_ne_zero` `IsWeierstrassDivision.congr_simp` `IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod`
`isWeierstrassFactorizationAt_iff` 📖	mathematical	—	`IsWeierstrassFactorizationAt` `Polynomial.IsDistinguishedAt` `IsUnit` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	—	—
`isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit` 📖	mathematical	—	`IsWeierstrassFactorization` `weierstrassDistinguished` `weierstrassUnit`	—	`exists_isWeierstrassFactorization`
`smul_weierstrassDiv` 📖	mathematical	—	`weierstrassDiv` `PowerSeries` `Algebra.toSMul` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule`	—	`IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisor.of_map_ne_zero` `IsWeierstrassDivisorAt.div_smul` `smul_zero`
`smul_weierstrassMod` 📖	mathematical	—	`weierstrassMod` `PowerSeries` `Algebra.toSMul` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra`	—	`IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisor.of_map_ne_zero` `IsWeierstrassDivisorAt.mod_smul` `smul_zero`
`weierstrassDistinguished_mul` 📖	mathematical	—	`weierstrassDistinguished` `PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial` `Polynomial.instMul`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit` `MulZeroClass.mul_zero` `IsWeierstrassFactorization.elim` `IsAdicComplete.toIsHausdorff` `IsWeierstrassFactorizationAt.mul`
`weierstrassDistinguished_smul` 📖	mathematical	—	`weierstrassDistinguished` `PowerSeries` `Algebra.toSMul` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id`	—	`Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_C` `MulZeroClass.mul_zero` `isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MulZeroClass.zero_mul` `IsWeierstrassFactorization.elim` `IsAdicComplete.toIsHausdorff` `IsWeierstrassFactorizationAt.smul`
`weierstrassDiv_zero` 📖	mathematical	—	`weierstrassDiv` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`weierstrassDiv_zero_right`
`weierstrassDiv_zero_left` 📖	mathematical	—	`weierstrassDiv` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring`	—	`IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisor.of_map_ne_zero` `IsWeierstrassDivisorAt.div_zero`
`weierstrassDiv_zero_right` 📖	mathematical	—	`weierstrassDiv` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`IsWeierstrassDivisor.of_map_ne_zero` `weierstrassDiv.eq_1` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`weierstrassMod_zero` 📖	mathematical	—	`weierstrassMod` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero`	—	`weierstrassMod_zero_right`
`weierstrassMod_zero_left` 📖	mathematical	—	`weierstrassMod` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `Polynomial` `Polynomial.instZero`	—	`IsAdicComplete.toIsPrecomplete` `IsWeierstrassDivisor.of_map_ne_zero` `IsWeierstrassDivisorAt.mod_zero`
`weierstrassMod_zero_right` 📖	mathematical	—	`weierstrassMod` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero`	—	`IsWeierstrassDivisor.of_map_ne_zero` `weierstrassMod.eq_1` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`weierstrassUnit_mul` 📖	mathematical	—	`weierstrassUnit` `PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit` `MulZeroClass.mul_zero` `IsWeierstrassFactorization.elim` `IsAdicComplete.toIsHausdorff` `IsWeierstrassFactorizationAt.mul`
`weierstrassUnit_smul` 📖	mathematical	—	`weierstrassUnit` `PowerSeries` `Algebra.toSMul` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `instAlgebra` `Algebra.id`	—	`Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_C` `MulZeroClass.mul_zero` `isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MulZeroClass.zero_mul` `IsWeierstrassFactorization.elim` `IsAdicComplete.toIsHausdorff` `IsWeierstrassFactorizationAt.smul`
`zero_weierstrassDiv` 📖	mathematical	—	`weierstrassDiv` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring`	—	`weierstrassDiv_zero_left`
`zero_weierstrassMod` 📖	mathematical	—	`weierstrassMod` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `Polynomial` `Polynomial.instZero`	—	`weierstrassMod_zero_left`

PowerSeries.IsWeierstrassDivision

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim` 📖	—	`PowerSeries.IsWeierstrassDivision`	—	—	`PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add` `PowerSeries.IsWeierstrassDivisor.of_map_ne_zero` `PowerSeries.IsWeierstrassDivisionAt.degree_lt` `PowerSeries.IsWeierstrassDivisionAt.eq_mul_add`
`eq_zero` 📖	mathematical	`PowerSeries.IsWeierstrassDivision` `PowerSeries` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero`	—	`elim` `PowerSeries.isWeierstrassDivisionAt_zero`
`isUnit_of_map_ne_zero` 📖	mathematical	`PowerSeries.IsWeierstrassDivision` `PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PowerSeries.X` `ENat.toNat` `PowerSeries.order` `IsLocalRing.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `PowerSeries.map` `IsLocalRing.residue`	`IsUnit`	—	`Ideal.instIsTwoSided_1` `PowerSeries.isUnit_iff_constantCoeff` `isUnit_map_iff` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsLocalRing.instIsLocalHomResidueFieldRingHomResidue` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `mul_comm` `PowerSeries.coeff_zero_eq_constantCoeff` `PowerSeries.coeff_map` `Finset.sum_singleton` `Finset.sum_subset` `add_zero` `PowerSeries.coeff_of_lt_order` `PowerSeries.order_finite_iff_ne_zero` `ENat.lt_lift_iff` `ENat.lift_eq_toNat_of_lt_top` `LE.le.lt_of_ne` `Finset.antidiagonal.fst_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Tactic.Contrapose.contrapose₄` `Finset.mem_singleton` `Finset.antidiagonal_congr` `MulZeroClass.zero_mul` `PowerSeries.coeff_mul` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Polynomial.coeff_eq_zero_of_degree_lt` `Polynomial.coeff_coe` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `PowerSeries.coeff_X_pow_self` `PowerSeries.map_X` `map_pow`
`isWeierstrassFactorization` 📖	mathematical	`PowerSeries.IsWeierstrassDivision` `PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PowerSeries.X` `ENat.toNat` `PowerSeries.order` `IsLocalRing.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `PowerSeries.map` `IsLocalRing.residue`	`PowerSeries.IsWeierstrassFactorization` `Polynomial` `Polynomial.instSub` `CommRing.toRing` `Polynomial.semiring` `Polynomial.X` `Units.val` `Units` `Units.instInv` `IsUnit.unit` `isUnit_of_map_ne_zero`	—	`PowerSeries.IsWeierstrassDivisionAt.degree_lt` `isUnit_of_map_ne_zero` `Polynomial.degree_X_pow` `IsLocalRing.toNontrivial` `Polynomial.degree_sub_eq_left_of_degree_lt` `Polynomial.natDegree.eq_1` `Polynomial.coeff_sub` `Polynomial.coeff_X_pow` `LT.lt.ne` `zero_sub` `NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClassIdeal` `PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem` `Polynomial.coeff_coe` `neg_mem_iff` `PowerSeries.coeff_X_pow` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Polynomial.Monic.sub_of_left` `Polynomial.monic_X_pow` `Units.isUnit` `PowerSeries.IsWeierstrassDivisionAt.eq_mul_add` `sub_eq_iff_eq_add` `mul_one` `IsUnit.mul_val_inv` `mul_assoc` `add_mul` `Distrib.rightDistribClass` `Polynomial.coe_sub` `Polynomial.coe_pow` `Polynomial.coe_X` `sub_mul`
`unique` 📖	mathematical	`PowerSeries.IsWeierstrassDivision`	`PowerSeries.weierstrassDiv` `IsAdicComplete.toIsPrecomplete` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `PowerSeries.weierstrassMod`	—	`elim` `IsAdicComplete.toIsHausdorff` `IsAdicComplete.toIsPrecomplete` `PowerSeries.isWeierstrassDivision_weierstrassDiv_weierstrassMod`

PowerSeries.IsWeierstrassDivisionAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`PowerSeries.IsWeierstrassDivisionAt`	`PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PowerSeries.instCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instAdd`	—	`LE.le.trans_lt` `Ideal.instIsTwoSided_1` `Polynomial.degree_add_le` `sup_lt_iff` `degree_lt` `eq_mul_add` `Polynomial.coe_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt`
`coeff_f_sub_r_mem` 📖	mathematical	`PowerSeries.IsWeierstrassDivisionAt` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map`	`CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap` `RingHom.id` `PowerSeries.instAddCommMonoid` `PowerSeries.instModule` `LinearMap.instFunLike` `PowerSeries.coeff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `PowerSeries.instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Polynomial.toPowerSeries`	—	`Ideal.instIsTwoSided_1` `eq_mul_add` `sub_eq_iff_eq_add` `PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal` `PowerSeries.coeff_of_lt_order_toNat` `lt_of_le_of_lt` `RingHom.instRingHomClass` `Ideal.mk_ker` `RingHom.mem_ker` `PowerSeries.coeff_map` `le_rfl`
`degree_lt` 📖	mathematical	`PowerSeries.IsWeierstrassDivisionAt`	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map`	—	—
`eq_mul_add` 📖	mathematical	`PowerSeries.IsWeierstrassDivisionAt`	`PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PowerSeries.instCommRing` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.toPowerSeries`	—	—
`smul` 📖	mathematical	`PowerSeries.IsWeierstrassDivisionAt`	`PowerSeries` `Algebra.toSMul` `CommRing.toCommSemiring` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `PowerSeries.instAlgebra` `Algebra.id` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra`	—	`LE.le.trans_lt` `Ideal.instIsTwoSided_1` `Polynomial.degree_smul_le` `degree_lt` `eq_mul_add` `Algebra.smul_def` `mul_add` `Distrib.leftDistribClass` `mul_left_comm` `Polynomial.coe_mul` `Polynomial.coe_C`

PowerSeries.IsWeierstrassDivisor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_map_ne_zero` 📖	mathematical	—	`PowerSeries.IsWeierstrassDivisor`	—	`eq_1` `Ideal.instIsTwoSided_1` `PowerSeries.IsWeierstrassDivisorAt.eq_1` `IsLocalRing.notMem_maximalIdeal` `PowerSeries.coeff_order` `Mathlib.Tactic.Contrapose.contrapose₄` `PowerSeries.coeff_map` `IsLocalRing.residue_eq_zero_iff`

PowerSeries.IsWeierstrassDivisorAt

Definitions

Name	Category	Theorems
`div` 📖	CompOp	7 math math: `div_coe_eq_zero`, `coeff_div`, `div_add`, `div_zero`, `isWeierstrassDivisionAt_div_mod`, `div_smul`, `coeff_div_sub_seq_mem`
`divCoeff` 📖	CompOp	1 math math: `coeff_div`
`mod'` 📖	CompOp	4 math math: `PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply`, `mod'_mk_eq_mod`, `Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply`, `mk_mod'_eq_self`
`seq` 📖	CompOp	5 math math: `coeff_seq_succ_sub_seq_mem`, `coeff_seq_mem`, `seq_one`, `seq_zero`, `coeff_div_sub_seq_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_div` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `div` `divCoeff`	—	`IsScalarTower.right`
`coeff_div_sub_seq_mem` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `DFunLike.coe` `LinearMap` `RingHom.id` `PowerSeries` `PowerSeries.instAddCommMonoid` `PowerSeries.instModule` `LinearMap.instFunLike` `PowerSeries.coeff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `PowerSeries.instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `div` `seq`	—	`IsScalarTower.right` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_div` `IsScalarTower.left` `Ideal.mul_top` `Ideal.instIsTwoSided_1` `SModEq.symm`
`coeff_seq_mem` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map`	`CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `LinearMap` `RingHom.id` `PowerSeries.instAddCommMonoid` `PowerSeries.instModule` `LinearMap.instFunLike` `PowerSeries.coeff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `PowerSeries.instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MvPowerSeries.instMul` `seq`	—	`Ideal.instIsTwoSided_1` `IsScalarTower.right` `pow_zero` `Ideal.one_eq_top` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `isUnit_shift` `seq.eq_2` `PowerSeries.eq_X_pow_mul_shift_add_trunc` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `sub_add_cancel_left` `mul_neg` `mul_assoc` `mul_right_comm` `add_mul` `Distrib.rightDistribClass` `IsUnit.mul_val_inv` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Polynomial.coeff_coe` `PowerSeries.coeff_trunc` `LE.le.not_gt` `zero_sub` `neg_mem_iff` `NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClassIdeal` `pow_succ'` `PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal'` `PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd`
`coeff_seq_succ_sub_seq_mem` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `DFunLike.coe` `LinearMap` `RingHom.id` `PowerSeries` `PowerSeries.instAddCommMonoid` `PowerSeries.instModule` `LinearMap.instFunLike` `PowerSeries.coeff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `PowerSeries.instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `seq`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1` `isUnit_shift` `seq.eq_2` `add_sub_cancel_left` `PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal'` `coeff_seq_mem` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd`
`div_add` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`div` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PowerSeries.instCommRing` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsAdicComplete.toIsPrecomplete` `PowerSeries.IsWeierstrassDivisionAt.add` `isWeierstrassDivisionAt_div_mod` `eq_of_mul_add_eq_mul_add` `IsAdicComplete.toIsHausdorff` `PowerSeries.IsWeierstrassDivisionAt.degree_lt` `PowerSeries.IsWeierstrassDivisionAt.eq_mul_add`
`div_coe_eq_zero` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map`	`div` `Polynomial.toPowerSeries` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `Semiring.toModule` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Ideal.instIsTwoSided_1` `IsAdicComplete.toIsPrecomplete` `isWeierstrassDivisionAt_div_mod` `eq_of_mul_add_eq_mul_add` `IsAdicComplete.toIsHausdorff` `MulZeroClass.mul_zero` `zero_add`
`div_smul` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`div` `PowerSeries` `Algebra.toSMul` `CommRing.toCommSemiring` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `PowerSeries.instAlgebra` `Algebra.id` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule`	—	`IsAdicComplete.toIsPrecomplete` `PowerSeries.IsWeierstrassDivisionAt.smul` `isWeierstrassDivisionAt_div_mod` `eq_of_mul_add_eq_mul_add` `IsAdicComplete.toIsHausdorff` `PowerSeries.IsWeierstrassDivisionAt.degree_lt` `PowerSeries.IsWeierstrassDivisionAt.eq_mul_add`
`div_zero` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`div` `PowerSeries` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsAdicComplete.toIsPrecomplete` `smul_zero` `zero_smul` `div_smul`
`eq_of_mul_add_eq_mul_add` 📖	—	`PowerSeries.IsWeierstrassDivisorAt` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PowerSeries.instCommRing` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	—	—	`Ideal.instIsTwoSided_1` `Polynomial.coe_sub` `mul_sub` `eq_sub_iff_add_eq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `eq_zero_of_mul_eq` `lt_of_le_of_lt` `Polynomial.degree_sub_le` `max_lt`
`eq_zero_of_mul_eq` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	`PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `Polynomial.instZero`	—	`Ideal.instIsTwoSided_1` `pow_zero` `Ideal.one_eq_top` `IsScalarTower.right` `lt_or_ge` `PowerSeries.eq_X_pow_mul_shift_add_trunc` `pow_succ'` `PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `Polynomial.coeff_coe` `Ideal.add_mem` `PowerSeries.coeff_X_pow_mul'` `LT.lt.not_ge` `lt_of_le_of_lt` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `le_rfl` `Polynomial.coeff_eq_zero_of_degree_lt` `lt_of_lt_of_le` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `isUnit_shift` `eq_sub_iff_add_eq` `mul_comm` `add_mul` `Distrib.rightDistribClass` `PowerSeries.coeff_X_pow_mul` `one_mul` `IsUnit.val_inv_mul` `mul_assoc` `PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal'` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Ideal.sub_mem` `PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'` `PowerSeries.ext` `IsHausdorff.haus'` `IsScalarTower.left` `SModEq.zero` `smul_eq_mul` `Ideal.mul_top` `Polynomial.coe_eq_zero_iff` `MulZeroClass.mul_zero`
`isUnit_shift` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`IsUnit` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map`	—	`Ideal.instIsTwoSided_1` `zero_add`
`isWeierstrassDivisionAt_div_mod` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`PowerSeries.IsWeierstrassDivisionAt` `div` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `mod`	—	`IsAdicComplete.toIsPrecomplete` `eq_or_ne` `IsHausdorff.subsingleton` `IsAdicComplete.toIsHausdorff` `PowerSeries.instSubsingleton` `IsPrecomplete.top` `Unique.instSubsingleton` `PowerSeries.isWeierstrassDivisionAt_zero` `PowerSeries.degree_trunc_lt` `Ideal.instIsTwoSided_1` `mod.eq_1` `add_comm` `sub_eq_iff_eq_add` `PowerSeries.ext` `Polynomial.coeff_coe` `PowerSeries.coeff_trunc` `IsHausdorff.haus'` `IsScalarTower.left` `IsScalarTower.right` `SModEq.zero` `smul_eq_mul` `Ideal.mul_top` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Ideal.sub_mem` `coeff_seq_mem` `not_lt` `PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal'` `coeff_div_sub_seq_mem`
`mk_mod'_eq_self` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`DFunLike.coe` `RingHom` `PowerSeries` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `PowerSeries.instRing` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instSingletonSet` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `PowerSeries.instCommRing` `RingHom.instFunLike` `Polynomial.toPowerSeries` `LinearMap` `RingHom.id` `Ideal.instHasQuotient_1` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Polynomial.commRing` `Submodule.Quotient.module'` `PowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `PowerSeries.instAlgebra` `Algebra.id` `PowerSeries.instModule` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsScalarTower.right` `Polynomial.module` `LinearMap.instFunLike` `mod'`	—	`Ideal.instIsTwoSided_1` `IsScalarTower.right` `Ideal.Quotient.mk_surjective` `IsAdicComplete.toIsPrecomplete` `mod'_mk_eq_mod` `Ideal.Quotient.mk_eq_mk_iff_sub_mem` `Ideal.mem_span_singleton'` `eq_sub_iff_add_eq` `mul_comm` `PowerSeries.IsWeierstrassDivisionAt.eq_mul_add` `isWeierstrassDivisionAt_div_mod`
`mod'_mk_eq_mod` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `PowerSeries` `Ideal` `PowerSeries.instSemiring` `Ideal.instHasQuotient_1` `PowerSeries.instCommRing` `Ideal.span` `Set` `Set.instSingletonSet` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Polynomial.commRing` `Submodule.Quotient.module'` `PowerSeries.instRing` `CommRing.toRing` `PowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `PowerSeries.instAlgebra` `Algebra.id` `PowerSeries.instModule` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `IsScalarTower.right` `Polynomial.module` `LinearMap.instFunLike` `mod'` `RingHom` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `mod` `IsAdicComplete.toIsPrecomplete`	—	`IsScalarTower.right` `Ideal.instIsTwoSided_1`
`mod_add` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`mod` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PowerSeries.instCommRing` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial` `Polynomial.instAdd`	—	`IsAdicComplete.toIsPrecomplete` `PowerSeries.IsWeierstrassDivisionAt.add` `isWeierstrassDivisionAt_div_mod` `eq_of_mul_add_eq_mul_add` `IsAdicComplete.toIsHausdorff` `PowerSeries.IsWeierstrassDivisionAt.degree_lt` `PowerSeries.IsWeierstrassDivisionAt.eq_mul_add`
`mod_coe_eq_self` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map`	`mod` `Polynomial.toPowerSeries` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `Semiring.toModule`	—	`Ideal.instIsTwoSided_1` `IsAdicComplete.toIsPrecomplete` `isWeierstrassDivisionAt_div_mod` `eq_of_mul_add_eq_mul_add` `IsAdicComplete.toIsHausdorff` `MulZeroClass.mul_zero` `zero_add`
`mod_smul` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`mod` `PowerSeries` `Algebra.toSMul` `CommRing.toCommSemiring` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `PowerSeries.instAlgebra` `Algebra.id` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra`	—	`IsAdicComplete.toIsPrecomplete` `PowerSeries.IsWeierstrassDivisionAt.smul` `isWeierstrassDivisionAt_div_mod` `eq_of_mul_add_eq_mul_add` `IsAdicComplete.toIsHausdorff` `PowerSeries.IsWeierstrassDivisionAt.degree_lt` `PowerSeries.IsWeierstrassDivisionAt.eq_mul_add`
`mod_zero` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`mod` `PowerSeries` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsAdicComplete.toIsPrecomplete` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial` `Polynomial.instZero`	—	`IsAdicComplete.toIsPrecomplete` `mod.congr_simp` `smul_zero` `zero_smul` `mod_smul`
`seq_one` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`seq` `PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `RingHom` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instInv` `IsUnit.unit` `isUnit_shift`	—	`Ideal.instIsTwoSided_1` `isUnit_shift` `MulZeroClass.mul_zero` `zero_add` `sub_zero`
`seq_zero` 📖	mathematical	`PowerSeries.IsWeierstrassDivisorAt`	`seq` `PowerSeries` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—

PowerSeries.IsWeierstrassFactorization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degree_eq_coe_lift_order_map` 📖	mathematical	`PowerSeries.IsWeierstrassFactorization`	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.lift` `PowerSeries.order` `IsLocalRing.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.map` `IsLocalRing.residue` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Top.top` `instTopENat` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.order_finite_iff_ne_zero` `map_ne_zero`	—	`PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top` `Ideal.IsMaximal.ne_top` `IsLocalRing.maximalIdeal.isMaximal`
`elim` 📖	—	`PowerSeries.IsWeierstrassFactorization`	—	—	`PowerSeries.IsWeierstrassFactorizationAt.isUnit` `PowerSeries.IsWeierstrassDivision.elim` `map_ne_zero` `isWeierstrassDivision` `Units.ext_iff`
`isWeierstrassDivision` 📖	mathematical	`PowerSeries.IsWeierstrassFactorization`	`PowerSeries.IsWeierstrassDivision` `PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PowerSeries.X` `ENat.toNat` `PowerSeries.order` `IsLocalRing.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `PowerSeries.map` `IsLocalRing.residue` `Units.val` `Units` `Units.instInv` `IsUnit.unit` `PowerSeries.IsWeierstrassFactorizationAt.isUnit` `IsLocalRing.maximalIdeal` `Polynomial` `Polynomial.instSub` `CommRing.toRing` `Polynomial.semiring` `Polynomial.X`	—	`PowerSeries.IsWeierstrassFactorizationAt.isUnit` `LT.lt.trans_eq` `Ideal.instIsTwoSided_1` `Polynomial.degree_sub_lt` `PowerSeries.order_finite_iff_ne_zero` `map_ne_zero` `degree_eq_coe_lift_order_map` `Polynomial.degree_X_pow` `IsLocalRing.toNontrivial` `ENat.lift_eq_toNat_of_lt_top` `Polynomial.Monic.ne_zero` `Polynomial.monic_X_pow` `Polynomial.Monic.leadingCoeff` `Polynomial.IsDistinguishedAt.monic` `PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt` `WithBot.charZero` `Nat.instCharZero` `PowerSeries.IsWeierstrassFactorizationAt.eq_mul` `mul_assoc` `IsUnit.mul_val_inv` `mul_one` `Polynomial.coe_sub` `Polynomial.coe_pow` `Polynomial.coe_X` `add_sub_cancel`
`map_ne_zero` 📖	—	`PowerSeries.IsWeierstrassFactorization`	—	—	`PowerSeries.IsWeierstrassFactorizationAt.map_ne_zero_of_ne_top` `Ideal.IsMaximal.ne_top` `IsLocalRing.maximalIdeal.isMaximal`
`natDegree_eq_toNat_order_map` 📖	mathematical	`PowerSeries.IsWeierstrassFactorization`	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ENat.toNat` `PowerSeries.order` `IsLocalRing.ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.map` `IsLocalRing.residue`	—	`PowerSeries.IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top` `Ideal.IsMaximal.ne_top` `IsLocalRing.maximalIdeal.isMaximal`
`unique` 📖	mathematical	`PowerSeries.IsWeierstrassFactorization`	`PowerSeries.weierstrassDistinguished` `PowerSeries.weierstrassUnit`	—	`elim` `IsAdicComplete.toIsHausdorff` `PowerSeries.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit`

PowerSeries.IsWeierstrassFactorizationAt

Definitions

Name	Category	Theorems
`algEquivQuotient` 📖	CompOp	2 math math: `algEquivQuotient_apply`, `algEquivQuotient_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquivQuotient_apply` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt`	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Polynomial.semiring` `Ideal.instHasQuotient_1` `Polynomial.commRing` `Ideal.span` `Set` `Set.instSingletonSet` `PowerSeries` `PowerSeries.instSemiring` `PowerSeries.instCommRing` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `Polynomial.algebraOfAlgebra` `Algebra.id` `PowerSeries.instAlgebra` `AlgEquiv.instFunLike` `algEquivQuotient` `Polynomial.toPowerSeries` `Ring.toSemiring` `PowerSeries.instRing` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.Quotient.algebra` `Ideal.quotientEquivAlgOfEq` `AlgHom` `Polynomial.ring` `AlgHom.funLike` `Ideal.quotientMapₐ` `Polynomial.coeToPowerSeries.algHom`	—	—
`algEquivQuotient_symm_apply` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt`	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `PowerSeries` `Ideal` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `PowerSeries.instCommRing` `Ideal.span` `Set` `Set.instSingletonSet` `Polynomial` `Polynomial.semiring` `Polynomial.commRing` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `PowerSeries.instAlgebra` `Algebra.id` `Polynomial.algebraOfAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `algEquivQuotient` `RingHom` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `LinearMap` `RingHom.id` `Polynomial.toPowerSeries` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Submodule.Quotient.module'` `PowerSeries.instRing` `PowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `Semiring.toModule` `Algebra.toSMul` `PowerSeries.instModule` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsScalarTower.right` `Polynomial.module` `LinearMap.instFunLike` `PowerSeries.IsWeierstrassDivisorAt.mod'` `Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt'` `isDistinguishedAt` `IsAdicComplete.toIsHausdorff` `Ideal.Quotient.algebra` `Ideal.quotientEquivAlgOfEq`	—	`Ideal.instIsTwoSided_1` `IsScalarTower.right` `Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt'` `isDistinguishedAt` `IsAdicComplete.toIsHausdorff` `Ideal.quotientEquivAlgOfEq_symm`
`degree_eq_coe_lift_order_map_of_ne_top` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt`	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.lift` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Top.top` `instTopENat` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.order_finite_iff_ne_zero` `map_ne_zero_of_ne_top`	—	`Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map` `isDistinguishedAt` `Mathlib.Tactic.Contrapose.contrapose₄` `Ideal.eq_top_of_isUnit_mem` `PowerSeries.isUnit_iff_constantCoeff` `isUnit` `eq_mul`
`eq_mul` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt`	`PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.toPowerSeries`	—	—
`isDistinguishedAt` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt`	`Polynomial.IsDistinguishedAt`	—	—
`isUnit` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt`	`IsUnit` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`map_ne_zero_of_ne_top` 📖	—	`PowerSeries.IsWeierstrassFactorizationAt`	—	—	`Ideal.Quotient.nontrivial_iff` `Ideal.instIsTwoSided_1` `eq_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Polynomial.polynomial_map_coe` `IsUnit.mul_left_eq_zero` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `isUnit` `Nat.cast_zero` `Polynomial.map_monic_ne_zero` `Polynomial.IsDistinguishedAt.monic` `isDistinguishedAt`
`mul` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt`	`PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial` `Polynomial.instMul`	—	`Polynomial.IsDistinguishedAt.mul` `isDistinguishedAt` `IsUnit.mul` `isUnit` `eq_mul` `Polynomial.coe_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`natDegree_eq_toNat_order_map_of_ne_top` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt`	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ENat.toNat` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `PowerSeries.map`	—	`Ideal.instIsTwoSided_1` `Polynomial.natDegree.eq_1` `PowerSeries.order_finite_iff_ne_zero` `map_ne_zero_of_ne_top` `degree_eq_coe_lift_order_map_of_ne_top` `ENat.lift_eq_toNat_of_lt_top` `WithBot.unbotD_coe`
`smul` 📖	mathematical	`PowerSeries.IsWeierstrassFactorizationAt` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`PowerSeries` `Algebra.toSMul` `PowerSeries.instSemiring` `PowerSeries.instAlgebra` `Algebra.id`	—	`isDistinguishedAt` `Algebra.smul_def` `IsUnit.mul` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `isUnit` `eq_mul` `Algebra.mul_smul_comm`

---

← Back to Index