Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-21 04:06 c71e67a9

View on Github →

feat(ring_theory/jacobson): definition of Jacobson rings (#3404)

Estimated changes

Modified src/data/equiv/ring.lean

added theorem ring_equiv.coe_ring_hom

Modified src/ring_theory/ideal_operations.lean

added theorem ideal.comap.is_maximal

added theorem ideal.comap_bot_le_of_injective

added theorem ideal.comap_le_iff_le_map

deleted theorem ideal.is_local.le_jacobson

deleted theorem ideal.is_local.mem_jacobson_or_exists_inv

deleted def ideal.is_local

deleted theorem ideal.is_local_of_is_maximal_radical

deleted theorem ideal.is_primary_of_is_maximal_radical

deleted def ideal.jacobson

deleted theorem ideal.jacobson_eq_top_iff

added theorem ideal.ker_le_comap

added theorem ideal.le_map_of_comap_le_of_surjective

added theorem ideal.map.is_maximal

added theorem ideal.map_Inf

added theorem ideal.map_eq_top_or_is_maximal_of_surjective

deleted theorem ideal.mem_jacobson_iff

added theorem ideal.mem_map_iff_of_surjective

added def ideal.order_iso_of_bijective

Modified src/ring_theory/ideals.lean

added theorem ideal.bot_is_maximal

Created src/ring_theory/jacobson.lean

added def ideal.is_jacobson

added theorem ideal.is_jacobson_iff_Inf_maximal

added theorem ideal.is_jacobson_iff_prime_eq

added theorem ideal.is_jacobson_iso

added theorem ideal.is_jacobson_of_surjective

added theorem ideal.radical_eq_jacobson

Created src/ring_theory/jacobson_ideal.lean

added theorem ideal.is_local.le_jacobson

added theorem ideal.is_local.mem_jacobson_or_exists_inv

added def ideal.is_local

added theorem ideal.is_local_of_is_maximal_radical

added theorem ideal.is_primary_of_is_maximal_radical

added theorem ideal.jacobson.is_maximal

added def ideal.jacobson

added theorem ideal.jacobson_eq_bot

added theorem ideal.jacobson_eq_top_iff

added theorem ideal.jacobson_mono

added theorem ideal.jacobson_top

added theorem ideal.le_jacobson

added theorem ideal.mem_jacobson_iff