Commit 2023-05-18 05:52 a3ae6e9e

View on Github →

feat port RingTheory.JacobsonIdeal (#4061)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/JacobsonIdeal.lean

added theorem Ideal.IsLocal.le_jacobson

added theorem Ideal.IsLocal.mem_jacobson_or_exists_inv

added theorem Ideal.comap_jacobson

added theorem Ideal.comap_jacobson_of_surjective

added theorem Ideal.eq_jacobson_iff_not_mem

added theorem Ideal.eq_jacobson_iff_sInf_maximal'

added theorem Ideal.eq_jacobson_iff_sInf_maximal

added theorem Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson

added theorem Ideal.isLocal_iff

added theorem Ideal.isLocal_of_isMaximal_radical

added theorem Ideal.isPrimary_of_isMaximal_radical

added theorem Ideal.isRadical_of_eq_jacobson

added theorem Ideal.isUnit_of_sub_one_mem_jacobson_bot

added def Ideal.jacobson

added theorem Ideal.jacobson_bot_polynomial_le_sInf_map_maximal

added theorem Ideal.jacobson_bot_polynomial_of_jacobson_bot

added theorem Ideal.jacobson_eq_bot

added theorem Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot

added theorem Ideal.jacobson_eq_self_of_isMaximal

added theorem Ideal.jacobson_eq_top_iff

added theorem Ideal.jacobson_idem

added theorem Ideal.jacobson_mono

added theorem Ideal.jacobson_radical_eq_jacobson

added theorem Ideal.jacobson_top

added theorem Ideal.le_jacobson

added theorem Ideal.map_jacobson_of_bijective

added theorem Ideal.map_jacobson_of_surjective

added theorem Ideal.mem_jacobson_bot

added theorem Ideal.mem_jacobson_iff

added theorem Ideal.radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot

added theorem Ideal.radical_le_jacobson