lean_workbook_plus_16781

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $n$ is even, say $n=2m$ , then $a^n=(a^m)^2 \geq 0$ because squares of real numbers are always nonnegative.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16781 (a : ℝ) (n : ℤ) : n % 2 = 0 → a ^ n ≥ 0   :=  by sorry

Source