Commit 2024-12-28 03:20 e8a30842

View on Github →

chore(Algebra): rename theorems for consistency (#20271) Taking chore material out of #16094 to make the diff cleaner. Moves: isSquare_one -> IsSquare.one isSquare_sq -> IsSquare.sq even_two_nsmul -> Even.two_nsmul isSumSq_sum_mul_self -> IsSumSq.mul_self

Estimated changes

added theorem IsSquare.one
added theorem IsSquare.sq
deleted theorem IsSquare_sq
deleted theorem isSquare_one