Integral_Domain_with_Characteristic_Zero
Provedcharacteristicintegral-domainproofwikiring-theory
In an integral domain with characteristic zero, every non-zero element has infinite order under ring addition.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Algebra.CharP.Basic
Formal statement
theorem Integral_Domain_with_Characteristic_Zero {R : Type _} [CommRing R] [IsDomain R] [CharZero R] (a : R) (ha : a ≠ 0) : ∀ n : ℕ, n ≠ 0 → n • a ≠ 0 := by sorrySource