Prove2Me

Characteristic_of_Field_is_Zero_or_Prime

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

characteristicfield-theoryproofwiki

Let FF be a field. Then the characteristic of FF is either zero or a prime number.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Algebra.CharP.Basic
Formal statement
theorem Characteristic_of_Field_is_Zero_or_Prime {F : Type _} [Field F] : ringChar F = 0 ∨ Nat.Prime (ringChar F) := by sorry
Source
https://proofwiki.org/wiki/Characteristic_of_Field_is_Zero_or_Prime

View graph