Ring_of_Integers_Modulo_Prime_is_Field_v2

Proved

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

fieldsmodular-arithmeticprime-numbersproofwikiring-theory

Let $m \in \Z: m \ge 2$ . Let $\struct {\Z_m, +, \times}$ be the ring of integers modulo $m$ . Then $m$ is prime $\struct {\Z_m, +, \times}$ is a field.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.ZMod.Basic

Formal statement

theorem Ring_of_Integers_Modulo_Prime_is_Field_v2 (p : ℕ) [hp : Fact (Nat.Prime p)] : ∀ (a : ZMod p), a ≠ 0 → IsUnit a := by sorry

Source

https://proofwiki.org/wiki/Ring_of_Integers_Modulo_Prime_is_Field

View graph