Criterion

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

Statistics

Metric	Count
Definitions	0
Theorems generalizedEisenstein, irreducible_of_eisenstein_criterion	2
Total	2

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generalizedEisenstein 📖	—	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring map CommSemiring.toSemiring CommRing.toCommSemiring algebraMap Monic IsPrimitive natDegree instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C leadingCoeff Monoid.toNatPow	—	—	RingHom.instRingHomClass Ideal.instIsTwoSided_1 degree_eq_zero_of_isUnit IsDomain.to_noZeroDivisors IsDomain.toNontrivial dvd_mul_right dvd_mul_left mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass modByMonic_eq_zero_iff_dvd Dvd.dvd.mul_left dvd_pow_self Dvd.dvd.mul_right add_zero zero_add ext Ideal.Quotient.eq_zero_iff_mem pow_two Ideal.mul_mem_mul RingHom.mem_ker coeff_map coeff_zero coeff_mul map_sum RingHomClass.toAddMonoidHomClass Finset.sum_congr Finset.sum_const_zero map_modByMonic zero_modByMonic
irreducible_of_eisenstein_criterion 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule leadingCoeff coeff WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id IsPrimitive	Irreducible Polynomial semiring	—	generalizedEisenstein Ideal.Quotient.isDomain Ideal.instIsTwoSided_1 map_X instIsDomain monic_X natDegree_pos_iff_degree_pos IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower IsScalarTower.right FractionRing.instFaithfulSMul instFaithfulSMul Ideal.Quotient.eq_zero_iff_mem map_C map_pow map_mul ext coeff_map coeff_C_mul coeff_X_pow mul_ite mul_one MulZeroClass.mul_zero sub_ite sub_zero leadingCoeff.eq_1 sub_self ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass coe_lt_degree coeff_eq_zero_of_natDegree_lt Ideal.zero_mem RingHom.instRingHomClass modByMonic_X C_eq_zero coeff_zero_eq_eval_zero RingHom.ker_comp_of_injective FaithfulSMul.algebraMap_injective Ideal.ext Ideal.mk_ker

---

← Back to Index