Zulip Chat Archive

Stream: new members

Topic: factorial base cases

Bo Qin (Aug 19 2025 at 14:55):

how come this gives error? math2001 exercise 6.2.7.7
math6.2.7.7.png

example {n : ℕ} (hn : 2 ≤ n) : Nat.Even (n !) := by
  induction_from_starting_point n, hn with k hk IH
  · use 1
    calc
      2 ! = 2 * 1 ! := by rw[factorial]
      _ = 2 * (1 * 0 !) := by rw[factorial]
      _ = 2 * 1 * 1 := by rw[factorial]
      _ = 2 * 1 := by ring
  · obtain ⟨x, hx⟩ := IH
    use k * x + x
    calc
      (k + 1)! = (k + 1) * k ! := by rw[factorial]
      _ = (k + 1) * (2 * x) := by rw[hx]
      _ = 2 * (k * x + x) := by ring