Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-17 00:07 21bdb787

View on Github →

feat(ring_theory/ideal_operations): jacobson radical, is_local, and primary ideals (#768)

Estimated changes

Modified src/ring_theory/ideal_operations.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.to_is_prime

added def ideal.is_primary

added theorem ideal.is_primary_inf

added theorem ideal.is_primary_of_is_maximal_radical

added theorem ideal.is_prime.comap

added theorem ideal.is_prime_radical

added def ideal.jacobson

added theorem ideal.jacobson_eq_top_iff

added theorem ideal.mem_jacobson_iff

added theorem ideal.mem_radical_of_pow_mem

Modified src/ring_theory/ideals.lean

added theorem ideal.mem_Inf