Commit 2025-01-23 11:42 e73fda6d

View on Github →

chore(Algebra/Group/Even): Clean up file (#20558)

  • Rename some theorems to remove primed variants
  • Move simp attribute from IsSquare.sq to Even.isSquare_pow for consistency
  • Remove unhelpful alias
  • Golf some proofs
  • Make notation consistent throughout proofs Moves: Even.nsmul -> Even.nsmul_right Even.nsmul' -> Even.nsmul_left Even.zsmul -> Even.zsmul_right Even.zsmul' -> Even.zsmul_left isSquare_zero -> IsSquare.zero Deletions: isSquare_of_exists_sq (prefer IsSquare.sq)

Estimated changes

modified theorem Even.isSquare_pow
modified theorem IsSquare.map
modified theorem IsSquare.mul_self
modified theorem IsSquare.pow
modified theorem IsSquare.sq
modified theorem IsSquare.zpow
modified theorem isSquare_iff_exists_sq
added theorem IsSquare.zero
deleted theorem isSquare_zero