Mathlib v3 is deprecated. Go to Mathlib v4

Theorem char_p.neg_one_ne_one

Modification history

2021-04-06 01:49
src/algebra/char_p/basic.lean
chore(algebra/char_p/basic): uniformise notation and weaken some assumptions (#6765) …
Modified char_p.neg_one_ne_oneView on Github →
2020-05-24 19:02
src/algebra/char_p.lean
feat(char_p): generalize zmod.neg_one_ne_one (#2796)
Added char_p.neg_one_ne_oneView on Github →