lean_workbook_plus_47133

Proved

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

Let $0\leq x,y,z<p$ then $y\equiv bx(mod p)$ and $z\equiv cy(mod p)\implies z\equiv bcx(mod p)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47133 (p : ℕ) (b c x y z : ℤ) (hp : 0 < p) (h : 0 ≤ x ∧ 0 ≤ y ∧ 0 ≤ z) (h2 : x < p ∧ y < p ∧ z < p) (h3 : y ≡ b * x [ZMOD p]) (h4 : z ≡ c * y [ZMOD p]) : z ≡ b * c * x [ZMOD p]   :=  by sorry

Source

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

View graph