theorem
other
other
twentyfive_decomp
show as:
view Lean formalization →
formal statement (Lean)
55theorem twentyfive_decomp : (25 : ℕ) = G5^2 := by decide