Lean-Workbook Plus 38068: Trigonometric inequality

Proved

WorkbookRestored.plus_38068

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

lean-workbookrestored-importssource-checked

Lean-Workbook Plus 38068: Real power of a power

For real $x\ge0$ and real $a,b$ , $x^{ab}=(x^a)^b$ . The formal statement uses Lean’s total real-power convention at base zero.

Source: Lean-Workbook row lean_workbook_plus_38068 (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.Real

Formal statement

theorem WorkbookRestored.plus_38068 {x : ℝ} (hx : 0 ≤ x) (a b : ℝ) : x ^ (a * b) = (x ^ a) ^ b   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_38068; immutable original Prove2Me node 6216b4dc-ed49-4a89-a143-b8060dccabdf

View graph