Commit 2024-10-20 21:29 1b6c758c

View on Github →

feat: negOnePow n = (-1 : ℤ) ^ n (#17967) and rename Int.coe_negOnePow to Int.cast_negOnePow for disambiguation

Estimated changes

Modified Mathlib/Algebra/Ring/NegOnePow.lean

added theorem Int.cast_negOnePow

added theorem Int.cast_negOnePow_natCast

deleted theorem Int.coe_negOnePow

added theorem Int.coe_negOnePow_natCast

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean