Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsEisensteinAt`, `IsWeaklyEisensteinAt`	2
Theorems `coeff_mem`, `irreducible`, `isWeaklyEisensteinAt`, `leading`, `mem`, `notMem`, `exists_mem_adjoin_mul_eq_pow_natDegree`, `exists_mem_adjoin_mul_eq_pow_natDegree_le`, `map`, `mem`, `mul`, `pow_natDegree_le_of_aeval_zero_of_monic_mem_map`, `pow_natDegree_le_of_root_of_monic_mem`, `isEisensteinAt_of_mem_of_notMem`, `leadingCoeff_notMem`, `dvd_pow_natDegree_of_aeval_eq_zero`, `dvd_pow_natDegree_of_eval₂_eq_zero`, `isEisensteinAt_iff`, `isWeaklyEisensteinAt_iff`, `isWeaklyEisensteinAt`	20
Total	22

Polynomial

Definitions

Name	Category	Theorems
`IsEisensteinAt` 📖	CompData	4 math math: `isEisensteinAt_iff`, `cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt`, `cyclotomic_comp_X_add_one_isEisensteinAt`, `Monic.isEisensteinAt_of_mem_of_notMem`
`IsWeaklyEisensteinAt` 📖	CompData	4 math math: `scaleRoots.isWeaklyEisensteinAt`, `IsEisensteinAt.isWeaklyEisensteinAt`, `isWeaklyEisensteinAt_iff`, `IsDistinguishedAt.toIsWeaklyEisensteinAt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_pow_natDegree_of_aeval_eq_zero` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `natDegree`	—	`dvd_pow_natDegree_of_eval₂_eq_zero` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `mul_comm`
`dvd_pow_natDegree_of_eval₂_eq_zero` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Monic` `eval₂` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `natDegree`	—	`natDegree_scaleRoots` `Ideal.mem_span_singleton` `IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem` `scaleRoots.isWeaklyEisensteinAt` `dvd_refl` `scaleRoots_eval₂_eq_zero` `injective_iff_map_eq_zero'` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `eval₂_at_apply` `monic_scaleRoots_iff` `le_rfl`
`isEisensteinAt_iff` 📖	mathematical	—	`IsEisensteinAt` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `leadingCoeff` `coeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id`	—	—
`isWeaklyEisensteinAt_iff` 📖	mathematical	—	`IsWeaklyEisensteinAt` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `coeff`	—	—

Polynomial.IsEisensteinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_mem` 📖	mathematical	`Polynomial.IsEisensteinAt`	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Polynomial.coeff`	—	`ne_iff_lt_or_gt` `mem` `Polynomial.coeff_eq_zero_of_natDegree_lt` `Ideal.zero_mem`
`irreducible` 📖	mathematical	`Polynomial.IsEisensteinAt` `CommRing.toCommSemiring` `Polynomial.IsPrimitive` `Polynomial.natDegree` `CommSemiring.toSemiring`	`Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	—	`Polynomial.irreducible_of_eisenstein_criterion` `leading` `mem` `Polynomial.coe_lt_degree` `Polynomial.natDegree_pos_iff_degree_pos` `notMem`
`isWeaklyEisensteinAt` 📖	mathematical	`Polynomial.IsEisensteinAt`	`Polynomial.IsWeaklyEisensteinAt`	—	`mem`
`leading` 📖	mathematical	`Polynomial.IsEisensteinAt`	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Polynomial.leadingCoeff`	—	—
`mem` 📖	mathematical	`Polynomial.IsEisensteinAt` `Polynomial.natDegree` `CommSemiring.toSemiring`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Polynomial.coeff`	—	—
`notMem` 📖	mathematical	`Polynomial.IsEisensteinAt`	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Polynomial.coeff`	—	—

Polynomial.IsWeaklyEisensteinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_adjoin_mul_eq_pow_natDegree` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.Monic` `Polynomial.IsWeaklyEisensteinAt` `Submodule.span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instSingletonSet`	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.natDegree` `Polynomial.map`	—	`eq_neg_of_add_eq_zero_left` `one_mul` `Polynomial.Monic.coeff_natDegree` `Polynomial.Monic.map` `Finset.sum_range` `Finset.sum_insert` `Finset.notMem_range_self` `Finset.range_add_one` `Polynomial.eval_eq_sum_range` `Polynomial.eval₂_eq_eval_map` `Polynomial.aeval_def` `Ideal.mem_span_singleton` `mem` `Polynomial.coeff_map` `lt_of_lt_of_le` `Polynomial.natDegree_map_le` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_assoc` `Finset.mul_sum` `neg_eq_neg_one_mul` `mul_comm` `Subalgebra.mul_mem` `Subalgebra.neg_mem` `Subalgebra.one_mem` `Subalgebra.sum_mem` `Subalgebra.algebraMap_mem` `Subalgebra.pow_mem` `Algebra.subset_adjoin` `Set.mem_singleton` `Zero.instNonempty` `Function.sometimes_spec`
`exists_mem_adjoin_mul_eq_pow_natDegree_le` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.Monic` `Polynomial.IsWeaklyEisensteinAt` `Submodule.span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instSingletonSet` `Polynomial.natDegree` `Polynomial.map` `algebraMap`	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `pow_add` `exists_mem_adjoin_mul_eq_pow_natDegree` `Subalgebra.mul_mem` `Subalgebra.pow_mem` `Algebra.subset_adjoin` `Set.mem_singleton` `mul_assoc`
`map` 📖	mathematical	`Polynomial.IsWeaklyEisensteinAt`	`Polynomial.map` `CommSemiring.toSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`Polynomial.isWeaklyEisensteinAt_iff` `Polynomial.coeff_map` `Ideal.mem_map_of_mem` `mem` `lt_of_lt_of_le` `Polynomial.natDegree_map_le`
`mem` 📖	mathematical	`Polynomial.IsWeaklyEisensteinAt` `Polynomial.natDegree` `CommSemiring.toSemiring`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Polynomial.coeff`	—	—
`mul` 📖	mathematical	`Polynomial.IsWeaklyEisensteinAt`	`Polynomial` `CommSemiring.toSemiring` `Polynomial.instMul`	—	`Polynomial.isWeaklyEisensteinAt_iff` `Polynomial.coeff_mul` `Ideal.sum_mem` `lt_or_ge` `Ideal.mul_mem_right` `Ideal.instIsTwoSided` `LT.lt.trans_le` `Polynomial.natDegree_mul_le` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_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` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `sub_eq_zero_of_eq` `Nat.cast_add` `Finset.HasAntidiagonal.mem_antidiagonal` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Ideal.mul_mem_left`
`pow_natDegree_le_of_aeval_zero_of_monic_mem_map` 📖	mathematical	`Polynomial.IsWeaklyEisensteinAt` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.Monic` `Polynomial.natDegree` `Polynomial.map` `algebraMap`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_natDegree_le_of_root_of_monic_mem` `map` `Polynomial.IsRoot.def` `Polynomial.eval₂_eq_eval_map` `Polynomial.aeval_def` `Polynomial.Monic.map` `Eq.le` `ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `pow_add` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1`
`pow_natDegree_le_of_root_of_monic_mem` 📖	mathematical	`Polynomial.IsWeaklyEisensteinAt` `CommRing.toCommSemiring` `Polynomial.IsRoot` `CommSemiring.toSemiring` `Polynomial.Monic` `Polynomial.natDegree`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `pow_add` `eq_neg_of_add_eq_zero_left` `one_mul` `Polynomial.Monic.coeff_natDegree` `Finset.sum_range` `Finset.sum_insert` `Finset.notMem_range_self` `Finset.range_add_one` `Polynomial.eval_eq_sum_range` `Polynomial.IsRoot.def` `neg_mem_iff` `NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClassIdeal` `Submodule.sum_mem` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `mem`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEisensteinAt_of_mem_of_notMem` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Polynomial.coeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id`	`Polynomial.IsEisensteinAt`	—	`leadingCoeff_notMem`
`leadingCoeff_notMem` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Polynomial.leadingCoeff`	—	`Ideal.ne_top_iff_one` `leadingCoeff`

Polynomial.scaleRoots

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isWeaklyEisensteinAt` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Polynomial.IsWeaklyEisensteinAt` `Polynomial.scaleRoots`	—	`Polynomial.coeff_scaleRoots` `Ideal.mul_mem_left` `Ideal.pow_mem_of_mem` `tsub_pos_iff_lt` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Polynomial.natDegree_scaleRoots`

---

← Back to Index