Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 12:41 863bf793

View on Github →

feat(data/padics): more valuations, facts about norms (#3790) Assorted lemmas about the p-adics. @jcommelin and I are adding algebraic structure here as part of the Witt vector development. Some of these declarations are stolen shamelessly from the perfectoid project. Coauthored by: Johan Commelin johan@commelin.net

Estimated changes

Modified src/data/padics/padic_norm.lean

added theorem padic_norm.padic_norm_p

added theorem padic_norm.padic_norm_p_lt_one

added theorem padic_norm.padic_norm_p_lt_one_of_prime

added theorem padic_norm.padic_norm_p_of_prime

Modified src/data/padics/padic_numbers.lean

modified theorem padic.cast_eq_of_rat_of_int

modified theorem padic.cast_eq_of_rat_of_nat

added theorem padic.norm_eq_pow_val

added def padic.valuation

added theorem padic.valuation_one

added theorem padic.valuation_p

added theorem padic.valuation_zero

added theorem padic_norm_e.norm_p

added theorem padic_norm_e.norm_p_lt_one

added theorem padic_norm_e.norm_p_pow

added theorem padic_seq.norm_eq_pow_val

deleted theorem padic_seq.norm_image

added theorem padic_seq.norm_values_discrete

added theorem padic_seq.val_eq_iff_norm_eq

added def padic_seq.valuation