Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-25 19:55 94fd41a2

View on Github →

refactor(data/padics/*): use [fact p.prime] to assume that p is prime (#2519)

Estimated changes

Modified docs/theories/padics.md

Modified src/data/padics/hensel.lean

modified theorem padic_polynomial_dist

Modified src/data/padics/padic_integers.lean

modified def padic_int

Modified src/data/padics/padic_norm.lean

modified theorem padic_val_rat.finite_int_prime_iff

modified theorem padic_val_rat_def

Modified src/data/padics/padic_numbers.lean

modified theorem padic.rat_dense'

modified theorem padic.rat_dense

modified def padic

modified theorem padic_norm_e.eq_of_norm_add_lt_left

modified theorem padic_norm_e.eq_of_norm_add_lt_right

modified def padic_norm_e

modified def padic_seq

Modified src/data/real/irrational.lean