lean_workbook_plus_44544
ProvedFind all such that or
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44544 (n : ℕ) : n ≡ 1 [ZMOD 6] ∨ n ≡ 5 [ZMOD 6] ↔ n % 6 = 1 ∨ n % 6 = 5 := by sorry
Source
Find all such that or
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_44544 (n : ℕ) : n ≡ 1 [ZMOD 6] ∨ n ≡ 5 [ZMOD 6] ↔ n % 6 = 1 ∨ n % 6 = 5 := by sorry