Multiplicative_Inverse_in_Ring_of_Integers_Modulo_m

Proved

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

modular-arithmeticmultiplicative-inverseproofwikiring-theory

Let $\struct {\Z_m, +_m, \times_m}$ be the ring of integers modulo $m$ . Then $\eqclass k m \in \Z_m$ has an inverse in $\struct {\Z_m, \times_m}$ $k \perp m$ .

Preamble

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

Formal statement

theorem Multiplicative_Inverse_in_Ring_of_Integers_Modulo_m (m : ℕ) [NeZero m] (k : ZMod m) : IsUnit k ↔ Nat.Coprime (ZMod.val k) m := by sorry

Source

https://proofwiki.org/wiki/Multiplicative_Inverse_in_Ring_of_Integers_Modulo_m

View graph