Commit 2023-03-15 10:21 5fa56426

View on Github →

feat: port Algebra.CharP.ExpChar (#2894)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CharP/ExpChar.lean

added theorem char_eq_expChar_iff

added theorem char_prime_of_ne_zero

added theorem char_zero_of_expChar_one

added theorem expChar_is_prime_or_one

added theorem expChar_one_iff_char_zero

added theorem expChar_one_of_char_zero