lean_workbook_plus_71663
ProvedNext, we have , which also only works for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71663 (x : ℕ) (h₀ : 2^x ≡ 1 [MOD 4]) : x = 0 := by sorry
Source
Next, we have , which also only works for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71663 (x : ℕ) (h₀ : 2^x ≡ 1 [MOD 4]) : x = 0 := by sorry