Commit 2024-10-27 15:34 17cb7894

View on Github →

feat(NumberTheory/Padics): p-adic valuation of casts (#17544) Lemmas about Padic.valuation applied to casts from various other rings to Qp

Estimated changes

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

added theorem Padic.valuation_intCast

added theorem Padic.valuation_natCast

added theorem Padic.valuation_ofNat

modified theorem Padic.valuation_one

modified theorem Padic.valuation_p

added theorem Padic.valuation_ratCast