Jacobson radical of polynomial ring

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

theorem Ring.jacobson_polynomial_eq_bot_of_jacobson_eq_bot {R : Type u_1} [CommRing R] (h : jacobson R = ⊥) : jacobson (Polynomial R) = ⊥

@[deprecated Ring.jacobson_polynomial_le_sInf_map_maximal (since := "2026-10-12")]

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})

@[deprecated Ring.jacobson_polynomial_eq_bot_of_jacobson_eq_bot (since := "2026-10-12")]

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