Commit 2022-04-15 15:03 c65bebb5

View on Github →

feat(number_theory/padics/padic_numbers): add padic.add_valuation (#12939) We define the p-adic additive valuation on Q_[p], as an add_valuation with values in with_top Z.

Estimated changes

Modified src/number_theory/padics/padic_numbers.lean

added theorem padic.add_valuation.apply

added theorem padic.add_valuation.map_add

added theorem padic.add_valuation.map_mul

added theorem padic.add_valuation.map_one

added theorem padic.add_valuation.map_zero

added def padic.add_valuation

added def padic.add_valuation_def

added theorem padic.valuation_map_add

added theorem padic.valuation_map_mul