Commit 2023-03-18 11:56 77a27b7f

View on Github →

feat: improvements in ExpChar (#2907)

  • Improve some proofs and documentation
  • Rename ExpChar.Prime to ExpChar.prime
  • I don't think this needs to be backported to Lean 3, since this cannot cause breaking changes.

Estimated changes

modified theorem expChar_is_prime_or_one