theorem
other
other
sigma_one_three_pow_one
show as:
view Lean formalization →
formal statement (Lean)
525theorem sigma_one_three_pow_one : sigma 1 (3 ^ 1) = 4 := by native_decide