Commit 2024-12-21 11:20 21a4ad33

View on Github →

chore: rename theorems for consistency (#20127) Taking chore material out of #16094 to make the diff cleaner. Moves: isSquare_mul_self -> IsSquare.mul_self even_add_self -> Even.add_self

Estimated changes

Modified Mathlib/Algebra/Group/Even.lean

added theorem IsSquare.mul_self

deleted theorem isSquare_mul_self

Modified Mathlib/Algebra/Order/Field/Power.lean

Modified Mathlib/Data/Fin/Parity.lean

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/LinearAlgebra/SymplecticGroup.lean