Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-18 14:10 739d28a6

View on Github →

refactor(ring_theory/multiplicity): replace padic_val with multiplicity (#495)

Estimated changes

Modified src/data/padics/padic_norm.lean

deleted theorem padic_val.dvd_of_padic_val_pos

deleted theorem padic_val.is_greatest

deleted theorem padic_val.le_padic_val_of_pow_dvd

deleted theorem padic_val.min_le_padic_val_add

deleted theorem padic_val.padic_val_eq_zero_of_coprime

deleted theorem padic_val.padic_val_eq_zero_of_not_dvd'

deleted theorem padic_val.padic_val_eq_zero_of_not_dvd

deleted theorem padic_val.padic_val_self

deleted theorem padic_val.pow_dvd_iff_le_padic_val

deleted theorem padic_val.pow_dvd_of_le_padic_val

deleted theorem padic_val.spec

deleted theorem padic_val.unique

deleted def padic_val

added theorem padic_val_rat.finite_int_prime_iff

added theorem padic_val_rat.le_padic_val_rat_add_of_le

modified theorem padic_val_rat.min_le_padic_val_rat_add

added theorem padic_val_rat.padic_val_rat_le_padic_val_rat_iff

modified theorem padic_val_rat.padic_val_rat_of_int

modified theorem padic_val_rat.padic_val_rat_self

added theorem padic_val_rat_def

Modified src/data/padics/padic_numbers.lean

Modified src/data/real/irrational.lean

added theorem irr_nrt_of_n_not_dvd_multiplicity

deleted theorem irr_nrt_of_n_not_dvd_padic_val

added theorem irr_sqrt_of_multiplicity_odd

deleted theorem irr_sqrt_of_padic_val_odd