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	4 math math: `IsDistinguishedAt.mul`, `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` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.constantCoeff` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	`ENat` `ENat.instNatCast` `Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.map` `Ideal.instIsTwoSided_1`	—	`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` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.constantCoeff` `MvPowerSeries.instMul` `Polynomial.toPowerSeries`	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `WithBot.natCast` `ENat.lift` `PowerSeries.order` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.map` `Ideal.instIsTwoSided_1` `ENat` `instLTENat` `Top.top` `instTopENat` `MvPowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `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'` `instReflLe` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.Quotient.semiring` `Ideal.instIsTwoSided_1` `Polynomial` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.natDegree`	—	`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` `MvPowerSeries.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'` `instReflLe` `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.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