Documentation Verification Report

Distinguished

📁 Source: Mathlib/RingTheory/Polynomial/Eisenstein/Distinguished.lean

Statistics

Metric	Count
Definitions `IsDistinguishedAt`	1
Theorems `coe_natDegree_eq_order_map`, `degree_eq_coe_lift_order_map`, `map_eq_X_pow`, `map_ne_zero_of_eq_mul`, `monic`, `mul`, `toIsWeaklyEisensteinAt`	7
Total	8

Polynomial

Definitions

Name	Category	Theorems
`IsDistinguishedAt` 📖	CompData	3 math math: `PowerSeries.isWeierstrassFactorizationAt_iff`, `PowerSeries.isDistinguishedAt_weierstrassDistinguished`, `PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt`

Polynomial.IsDistinguishedAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_natDegree_eq_order_map` 📖	mathematical	`Polynomial.IsDistinguishedAt` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `PowerSeries` `PowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.constantCoeff` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	`ENat` `ENat.instNatCast` `Polynomial.natDegree` `PowerSeries.order` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `PowerSeries.map`	—	`Ideal.instIsTwoSided_1` `Polynomial.natDegree.eq_1` `PowerSeries.order_finite_iff_ne_zero` `map_ne_zero_of_eq_mul` `degree_eq_coe_lift_order_map` `ENat.coe_lift`
`degree_eq_coe_lift_order_map` 📖	mathematical	`Polynomial.IsDistinguishedAt` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `PowerSeries` `PowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.constantCoeff` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	`Polynomial.degree` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `ENat.lift` `PowerSeries.order` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `PowerSeries.map` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Top.top` `instTopENat` `PowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `PowerSeries.order_finite_iff_ne_zero` `map_ne_zero_of_eq_mul`	—	`nontrivial_iff` `Ideal.zero_mem` `Ideal.instIsTwoSided_1` `PowerSeries.order_finite_iff_ne_zero` `map_ne_zero_of_eq_mul` `Polynomial.degree_eq_natDegree` `Polynomial.Monic.ne_zero` `monic` `WithBot.charZero` `Nat.instCharZero` `ENat.coe_lift` `PowerSeries.order_eq_nat` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_eq_X_pow` `Polynomial.polynomial_map_coe` `Polynomial.coe_pow` `Polynomial.coe_X` `PowerSeries.coeff_X_pow_mul'` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `PowerSeries.coeff_zero_eq_constantCoeff`
`map_eq_X_pow` 📖	mathematical	`Polynomial.IsDistinguishedAt`	`Polynomial.map` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Polynomial.ext` `Ideal.instIsTwoSided_1` `Polynomial.coeff_map` `Polynomial.Monic.leadingCoeff` `monic` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Polynomial.coeff_X_pow` `lt_or_gt_of_ne` `Polynomial.IsWeaklyEisensteinAt.mem` `toIsWeaklyEisensteinAt` `Polynomial.coeff_eq_zero_of_natDegree_lt` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`map_ne_zero_of_eq_mul` 📖	—	`Polynomial.IsDistinguishedAt` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `PowerSeries` `PowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.constantCoeff` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	—	—	`Ideal.instIsTwoSided_1` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_eq_X_pow` `Polynomial.polynomial_map_coe` `Polynomial.coe_pow` `Polynomial.coe_X` `PowerSeries.coeff_X_pow_mul'` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `PowerSeries.coeff_zero_eq_constantCoeff` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`monic` 📖	mathematical	`Polynomial.IsDistinguishedAt`	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`mul` 📖	mathematical	`Polynomial.IsDistinguishedAt`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instMul`	—	`Polynomial.IsWeaklyEisensteinAt.mul` `toIsWeaklyEisensteinAt` `Polynomial.Monic.mul` `monic`
`toIsWeaklyEisensteinAt` 📖	mathematical	`Polynomial.IsDistinguishedAt`	`Polynomial.IsWeaklyEisensteinAt` `CommRing.toCommSemiring`	—	—

---

← Back to Index