Theorem Int.isSquare_iff_nonneg_even_factorization

Modification history

2026-08-17 17:06
Mathlib/Data/Nat/Factorization/Defs.lean
feat(NumberTheory/Padics/PadicVal/Basic): Locally square rational numbers are squares (#42511) …
Added Int.isSquare_iff_nonneg_even_factorizationView on Github →