Commit 2023-11-28 12:41 88b4f4c7

View on Github →

feat: Relax arguments of going-up theorems. (#8645)

Estimated changes

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.exists_ideal_comap_le_prime

modified theorem Ideal.exists_ideal_over_maximal_of_isIntegral

deleted theorem Ideal.exists_ideal_over_prime_of_isIntegral'

added theorem Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain

added theorem Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime

added theorem Ideal.map_eq_top_iff

added theorem Ideal.map_eq_top_iff_of_ker_le