lean_workbook_plus_3649
ProvedFind such that and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3649 (x y : ℕ) (hx: 4^x ≡ 1 [ZMOD 9]) (hy: 2^y ≡ 0 [ZMOD 7]) : x = 3 ∧ y = 3 := by sorry
Source
Find such that and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_3649 (x y : ℕ) (hx: 4^x ≡ 1 [ZMOD 9]) (hy: 2^y ≡ 0 [ZMOD 7]) : x = 3 ∧ y = 3 := by sorry