Theorem Rat.isSquare_iff_even_factorization

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.isSquare_iff_even_factorizationView on Github →