Theorem char_p.char_ne_zero_of_fintype
Modification history
2022-08-11 16:08
src/algebra/char_p/basic.lean
feat(algebra/char_p): use `finite` instead of `fintype` (#16002) …
Deleted char_p.char_ne_zero_of_fintypeView on Github →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.char_ne_zero_of_fintypeView on Github →