Theorem Int.eq_of_squarefree_of_isSquare_mul

Modification history

2026-10-21 19:58
Mathlib/RingTheory/Int/Basic.lean
feat(Algebra/QuadraticAlgebra): classify quadratic algebras over ℚ (#42393) …
Added Int.eq_of_squarefree_of_isSquare_mulView on Github →