← Copula mathematical handbook

Jacobson radical of polynomial ring

theorem Ideal.jacobson_bot_polynomial_le_sInf_map_maximal {R : Type u_1} [CommRing R] : ⊥.jacobson ≤ sInf (map Polynomial.C '' {J : Ideal R | J.IsMaximal})

theorem Ideal.jacobson_bot_polynomial_of_jacobson_bot {R : Type u_1} [CommRing R] (h : ⊥.jacobson = ⊥) : ⊥.jacobson = ⊥