Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-13 13:42 a770ee5a

View on Github →

fix(data/padics/padic_rationals): fix proof

Estimated changes

Modified data/padics/padic_rationals.lean

modified theorem padic.cast_eq_of_rat

modified theorem padic.complete

modified theorem padic.exi_rat_seq_conv

modified def padic.mk

modified theorem padic.rat_dense

modified theorem padic_norm_e.nonarchimedean

modified theorem padic_norm_e.sub_rev

modified theorem padic_norm_e.zero_def

modified def padic_norm_e

modified theorem padic_seq.norm_equiv

modified theorem padic_seq.norm_nonzero_of_not_equiv_zero

modified theorem padic_seq.stationary