Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-22 00:27 219e2981

View on Github →

feat(ring_theory/discrete_valuation_ring): add DVR (#3476)

Estimated changes

Modified src/algebra/associated.lean

added theorem dvd_dvd_iff_associated

added theorem dvd_dvd_of_associated

added theorem dvd_of_associated

Created src/ring_theory/discrete_valuation_ring.lean

added theorem discrete_valuation_ring.associated_of_irreducible

added theorem discrete_valuation_ring.exists_irreducible

added theorem discrete_valuation_ring.iff_PID_with_one_nonzero_prime

added theorem discrete_valuation_ring.irreducible_iff_uniformiser

added theorem discrete_valuation_ring.not_a_field

Modified src/ring_theory/ideals.lean

added theorem ideal.maximal_of_no_maximal

added theorem ideal.span_singleton_eq_span_singleton

added theorem ideal.span_singleton_mul_left_unit

added theorem ideal.span_singleton_mul_right_unit

added theorem local_of_unique_nonzero_prime

added theorem local_ring.eq_maximal_ideal

added theorem local_ring.le_maximal_ideal

deleted theorem local_ring.max_ideal_unique

added theorem local_ring.maximal_ideal_unique