Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_unit_iff_not_dvd_char_of_ring_char_ne_zero

Modification history

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