Commit 2023-04-05 11:14 333d55a7

View on Github →

feat: port Algebra.CharP.CharAndCard (#3285)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CharP/CharAndCard.lean

added theorem isUnit_iff_not_dvd_char

added theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero

added theorem not_isUnit_prime_of_dvd_card

added theorem prime_dvd_char_iff_dvd_card