From ab0dad50264f21acdc1356f357cc73ca1513bdda Mon Sep 17 00:00:00 2001 From: Hanson Char Date: Sun, 13 Jul 2025 10:53:54 -0700 Subject: [PATCH] Add missing "by" in theorem Int.ModEq.pow --- .../03_Modular_Arithmetic_Theory.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Math2001/03_Parity_and_Divisibility/03_Modular_Arithmetic_Theory.lean b/Math2001/03_Parity_and_Divisibility/03_Modular_Arithmetic_Theory.lean index 5b65027a..0daef2be 100644 --- a/Math2001/03_Parity_and_Divisibility/03_Modular_Arithmetic_Theory.lean +++ b/Math2001/03_Parity_and_Divisibility/03_Modular_Arithmetic_Theory.lean @@ -54,7 +54,7 @@ theorem Int.ModEq.pow_two (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := b theorem Int.ModEq.pow_three (h : a ≡ b [ZMOD n]) : a ^ 3 ≡ b ^ 3 [ZMOD n] := by sorry -theorem Int.ModEq.pow (k : ℕ) (h : a ≡ b [ZMOD n]) : a ^ k ≡ b ^ k [ZMOD n] := +theorem Int.ModEq.pow (k : ℕ) (h : a ≡ b [ZMOD n]) : a ^ k ≡ b ^ k [ZMOD n] := by sorry -- we'll prove this later in the book