Commit 2025-06-28 23:55 c953365a

View on Github →

feat(Data/Sign): even and odd powers (#26495) Odd powers are the identity function, even powers on non-zero signs are always 1.

Estimated changes

Modified Mathlib/Data/Sign.lean

added theorem SignType.pow_even

added theorem SignType.pow_odd

added theorem SignType.zpow_even

added theorem SignType.zpow_odd