lean_workbook_plus_44405

Proved

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

For integers $a,x,y$ and prime number $p$ , where $p$ doesn't divide $a$ , prove that if $xa \equiv ya \pmod p$ and $0 < x,y \leq p$ , then $x=y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44405 (a x y p : ℤ) (hp : Prime p) (hpa : ¬ p ∣ a) (h0 : 0 < x ∧ 0 < y) (hxp : x ≤ p) (hyp : y ≤ p) (h : x * a ≡ y * a [ZMOD p]) : x ≡ y [ZMOD p]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph