Commit 2023-12-25 18:05 5ca2c4b1

View on Github →

feat(Algebra/CharP/ExpChar): add expChar[_pow]_pos (#9260) ... which states that (the power of) exponential characteristic is positive.

Estimated changes

added theorem expChar_pos
added theorem expChar_pow_pos