mathlib

b248481b - chore(algebra/char_zero): add `∀ n : ℕ, (n + 1 : α) ≠ 0` (#2644)