Theorem Padic.valuation_ratCast

Modification history

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