mathlib

6d3ca07a - feat(data/zmod/basic): `-1 : zmod n` lifts to `n - 1` (#13665)

feat(data/zmod/basic): `-1 : zmod n` lifts to `n - 1` (#13665) This PR adds a lemma stating that `-1 : zmod n` lifts to `n - 1 : R` for any ring `R`. The proof is surprisingly painful, but maybe someone can find a nicer way?