Commit 2026-08-17 17:06 7ab00b28

feat(NumberTheory/Padics/PadicVal/Basic): Locally square rational numbers are squares (#42511) In the ongoing formalization of Hasse-Minkowski Theorem on quadratic forms, we need the fact that a non-negative rational number having even p-adic valuations for all prime p is a square. This is added as isSquare_of_even_factorization in the Rat namespace in NumberTheory/Padics/PadicVal/Basic.lean in the PR. Also add preliminary lemmasnum_or_den_zero_padicVal num_den_even_padicVal_of_even_padicVal. As preliminary results, add analogous theorems for natural numbers and integers Nat.isSquare_of_even_factorization Int.isSquare_of_nonneg_of_even_factorization in Data/Nat/Factorization/Defs.lean.