Theorem ZMod.add_self_eq_zero_iff_eq_zero

Modification history

2023-07-31 15:32
Mathlib/Data/ZMod/Basic.lean
feat: `a + a = 0 ↔ a = 0` in `ZMod n` for `n` odd (#6086) …
Added ZMod.add_self_eq_zero_iff_eq_zeroView on Github →