Theorem Ideal.exists_ideal_over_prime_of_is_integral'

Modification history

2023-08-28 19:47

Mathlib/RingTheory/Ideal/Over.lean

chore: tidy various files (#6577)

Deleted Ideal.exists_ideal_over_prime_of_is_integral'View on Github →

2023-05-23 13:58

Mathlib/RingTheory/Ideal/Over.lean

feat: port RingTheory.Ideal.Over (#4270)

Added Ideal.exists_ideal_over_prime_of_is_integral'View on Github →