mathlib

c6aab262 - feat(algebra/invertible): invertible_of_ring_char_not_dvd (#2775)

feat(algebra/invertible): invertible_of_ring_char_not_dvd (#2775) ``` def invertible_of_ring_char_not_dvd {R : Type*} [field R] {t : ℕ} (not_dvd : ¬(ring_char R ∣ t)) : invertible (t : R) ``` Co-authored-by: Johan Commelin <johan@commelin.net>