Theorem Rat.num_den_even_padicVal_of_even_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_den_even_padicVal_of_even_padicValView on Github →