Commit 2025-04-18 12:50 aa3e7620

View on Github →

chore: rename {Irreducible,Prime}.not_square (#24136)

Estimated changes

Modified Mathlib/Algebra/Group/Irreducible/Lemmas.lean

added theorem Irreducible.not_isSquare

deleted theorem Irreducible.not_square

modified theorem IsSquare.not_irreducible

Modified Mathlib/Algebra/Prime/Lemmas.lean

modified theorem IsSquare.not_prime

added theorem Prime.not_isSquare

deleted theorem Prime.not_square

Modified Mathlib/Data/Real/Irrational.lean