Prove2Me

Lean-Workbook Plus 34718: Trigonometric identity

Proved
WorkbookRestored.plus_34718

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

Lean-Workbook Plus 34718: Fourth power of the imaginary unit

For complex q,eq,e with q=iq=i and e=4e=4, qe=1q^e=1. The formal exponent is complex, and at the integer value four it agrees with the usual fourth power.

Source: Lean-Workbook row lean_workbook_plus_34718 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
Formal statement
theorem WorkbookRestored.plus_34718  (q e : ℂ)
  (h₀ : q = Complex.I)
  (h₁ : e = 4) :
  q^e = 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_34718; immutable original Prove2Me node acc4dae6-7b29-42c4-9f04-49279b9670d4

View graph