Theorem Int.cast_negOnePow

Modification history

2025-03-29 10:26
Mathlib/Algebra/Field/NegOnePow.lean
feat: generalize Mathlib.Algebra.Group+Ring+Field (#23143) …
Modified Int.cast_negOnePowView on Github →
2025-02-14 05:38
Mathlib/Algebra/Field/NegOnePow.lean
chore(Data/ZMod/Basic): don't import `Field` (#21317)
Modified Int.cast_negOnePowView on Github →
2024-10-20 21:29
Mathlib/Algebra/Ring/NegOnePow.lean
feat: `negOnePow n = (-1 : ℤ) ^ n` (#17967) …
Added Int.cast_negOnePowView on Github →