Theorem Rat.num_or_den_zero_padicVal

Modification history

2026-08-17 17:06
Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
feat(NumberTheory/Padics/PadicVal/Basic): Locally square rational numbers are squares (#42511) …
Added Rat.num_or_den_zero_padicValView on Github →