Euler’s congruence modulo 77

Proved

WorkbookRestored.plus_12936

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

The integer congruence $2^{\varphi(77)}\equiv1\pmod{77}$ holds.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_12936 (Apache-2.0).

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Nat.Totient
import Mathlib.Data.Int.ModEq
open Nat

Formal statement

theorem WorkbookRestored.plus_12936 : 2 ^ (Nat.totient 77) ≡ 1 [ZMOD 77]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_12936; original Prove2Me node cb5ba78b-4758-4924-bded-2ad61eb21903; Apache-2.0

View graph