Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-14 03:22 1e9f6646

View on Github →

refactor(ring_theory/discrete_valuation_ring): discrete_valuation_ring.add_val as an add_valuation (#6660) Refactors discrete_valuation_ring.add_val to be an enat-valued add_valuation.

Estimated changes

Modified src/algebra/squarefree.lean

Modified src/ring_theory/discrete_valuation_ring.lean

modified theorem discrete_valuation_ring.add_val_add

added theorem discrete_valuation_ring.add_val_eq_top_iff

modified theorem discrete_valuation_ring.add_val_le_iff_dvd

modified theorem discrete_valuation_ring.add_val_mul

modified theorem discrete_valuation_ring.add_val_pow

deleted theorem discrete_valuation_ring.add_val_spec

modified theorem discrete_valuation_ring.add_val_zero

added theorem discrete_valuation_ring.exists_prime

Modified src/ring_theory/multiplicity.lean

added theorem multiplicity.eq_of_associated_left

added theorem multiplicity.eq_of_associated_right

deleted theorem multiplicity.multiplicity_le_multiplicity_of_dvd

added theorem multiplicity.multiplicity_le_multiplicity_of_dvd_left

added theorem multiplicity.multiplicity_le_multiplicity_of_dvd_right