lean_workbook_plus_24237
ProvedSuppose is a finite ring. Show that for each there is a positive integer such that . Here
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24237 (R : Type*) [Ring R] [Finite R] (x : R) : ∃ n : ℕ, n • x = 0 := by sorry
Source