Theorem Padic.valuation_natCast

Modification history

2024-10-27 15:34
Mathlib/NumberTheory/Padics/PadicNumbers.lean
feat(NumberTheory/Padics): p-adic valuation of casts (#17544) …
Added Padic.valuation_natCastView on Github →