lean_workbook_plus_47050

Proved

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

For each positive number $a$ , prove that its multiplicative inverse $a^{-1}$ is also positive.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47050 (a : ℝ) (ha : 0 < a) : 0 < a⁻¹   :=  by sorry

Source