Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-12 02:38 2974a9f9

View on Github →

feat(ring_theory): every division_ring is_noetherian (#7661)

Estimated changes

Modified src/ring_theory/ideal/basic.lean

modified theorem ideal.bot_is_maximal

modified theorem ideal.eq_bot_of_prime

modified theorem ideal.eq_bot_or_top

added theorem ideal.span_one

modified theorem ideal.span_singleton_one

Modified src/ring_theory/ideal/operations.lean

Modified src/ring_theory/principal_ideal_domain.lean

modified theorem principal_ideal_ring.is_maximal_of_irreducible