Theorem Irreducible.not_isSquare

Modification history

2025-04-18 12:50
Mathlib/Algebra/Group/Irreducible/Lemmas.lean
chore: rename {Irreducible,Prime}.not_square (#24136)
Added Irreducible.not_isSquareView on Github →