Ideal.map_le_jacobson_bot_of_isIntegral
Extension to an integral algebra preserves containment in the Jacobson radical.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u v
namespace IdealLean source · statement
theorem map_le_jacobson_bot_of_isIntegral {R : Type u} {S : Type v}
[CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S]
{I : Ideal R} (hI : I ≤ jacobson ⊥) :
I.map (algebraMap R S) ≤ jacobson ⊥