Commit 2024-01-10 20:21 fd4eb93d

View on Github →

feat(Algebra/CharP/ExpChar): add more results for ExpChar parallel to CharP (#9573)

Estimated changes

added theorem CharP.exists'
added theorem ExpChar.congr
added theorem ExpChar.eq
added theorem ExpChar.exists_unique
added theorem ringExpChar.eq
added theorem ringExpChar.eq_iff
added theorem ringExpChar.eq_one
added theorem ringExpChar.of_eq