Mathlib v3 is deprecated. Go to Mathlib v4

Theorem char_p.ring_char_ne_zero_of_finite

Modification history

2022-08-11 16:08
src/algebra/char_p/basic.lean
feat(algebra/char_p): use `finite` instead of `fintype` (#16002) …
Added char_p.ring_char_ne_zero_of_finiteView on Github →