Theorem Rat.padicValuation_le_one_iff

Modification history

2025-08-15 22:00

Mathlib/NumberTheory/Padics/PadicNumbers.lean

feat(NumberTheory/Padics): {Int,Rat}.padicValuation (#27667) …

Added Rat.padicValuation_le_one_iff View on Github →