Zulip Chat Archive

Stream: new members

Topic: modeq


view this post on Zulip Scott Morrison (Feb 27 2019 at 02:38):

Reasonable proof of lemma foo {k : ℕ} (h : k ≡ 1 [MOD 2]) : k ≡ 1 [MOD 4] ∨ k ≡ 3 [MOD 4] := and similar?

view this post on Zulip Scott Morrison (Feb 27 2019 at 02:46):

I guess

@[simp] lemma modeq_add_self (a b n : ℕ) : (a + n ≡ b [MOD n]) ↔ (a ≡ b [MOD n]) := sorry

lemma foo : Π {k : ℕ} (h : k ≡ 1 [MOD 2]), k ≡ 1 [MOD 4] ∨ k ≡ 3 [MOD 4]
| 0 h := by cases h
| 1 h := or.inl rfl
| 2 h := by cases h
| 3 h := or.inr rfl
| (n+4) h :=
begin
  rw modeq_add_self,
  erw modeq_add_self at h,
  erw modeq_add_self at h,
  exact foo h
end

works. Anything better?


Last updated: May 14 2021 at 13:24 UTC