Polynomial

📁 Source: Mathlib/RingTheory/Jacobson/Polynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems jacobson_bot_polynomial_le_sInf_map_maximal, jacobson_bot_polynomial_of_jacobson_bot	2
Total	2

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
jacobson_bot_polynomial_le_sInf_map_maximal 📖	mathematical	—	Ideal Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring Polynomial.ring CommRing.toRing Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule jacobson Bot.bot Polynomial.semiring Submodule.instBot InfSet.sInf Submodule.instInfSet Set.image map RingHom RingHom.instFunLike Polynomial.C setOf IsMaximal	—	le_sInf jacobson_mono bot_le le_of_eq eq_bot_iff Polynomial.coeff_X_one NeZero.one IsDomain.toNontrivial instIsTwoSided_1 Quotient.isDomain IsMaximal.isPrime' Polynomial.coeff_add Polynomial.mul_coeff_zero Polynomial.coeff_X_zero MulZeroClass.mul_zero Polynomial.coeff_one_zero zero_add map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AddRightCancelSemigroup.toIsRightCancelAdd Polynomial.instNoZeroDivisors Quotient.noZeroDivisors Polynomial.eq_C_of_degree_eq_zero Polynomial.degree_eq_zero_of_isUnit mem_jacobson_bot jacobson_eq_iff_jacobson_quotient_eq_bot map_bot map_jacobson_of_bijective RingEquiv.bijective
jacobson_bot_polynomial_of_jacobson_bot 📖	mathematical	jacobson CommRing.toRing Bot.bot Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ring.toSemiring	Polynomial Polynomial.ring Polynomial.semiring	—	eq_bot_iff le_trans jacobson_bot_polynomial_le_sInf_map_maximal Submodule.mem_bot Polynomial.ext mem_sInf mem_map_C_iff Polynomial.coeff_zero

---

← Back to Index