mathlib

cea8c65a - feat(algebra/char_p/exp_char): basics about the exponential characteristic (#6671)

feat(algebra/char_p/exp_char): basics about the exponential characteristic (#6671) This file contains the definition and a few basic facts pertaining to the exponential characteristic of an integral domain.