Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_unit_iff_not_dvd_char

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) …
Modified is_unit_iff_not_dvd_charView on Github →
2022-06-12 16:53
src/algebra/char_p/char_and_card.lean
feat(number_theory/legendre_symbol/auxiliary, *): add/move lemmas in/to various files, delete `auxiliary.lean` (#14572) …
Added is_unit_iff_not_dvd_charView on Github →