theorem
proved
term proof
W_endo_at_2
show as:
view Lean formalization →
formal statement (Lean)
41theorem W_endo_at_2 : W_endo 2 = 7 := by native_decide
proof body
Term-mode proof.
42
43/-- For D = 4: W_endo = 39. -/