Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-06 10:56 9c86e381

View on Github →

refactor(ring_theory/ideal/operations.lean): make is_prime.comap an instance (#7518)

Estimated changes

Modified src/algebraic_geometry/prime_spectrum.lean

Modified src/ring_theory/dedekind_domain.lean

Modified src/ring_theory/ideal/operations.lean

deleted theorem ideal.is_prime.comap