A real positive definite matrix is positive definite over $\mathbb{C}$

Proved

Matrix.PosDef.map_ofReal

by Mazecto · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebra

Let $M$ be a real symmetric positive definite $n\times n$ matrix. Then $M$ , viewed as a complex matrix, is Hermitian positive definite: $z^*Mz>0$ for every nonzero $z\in\mathbb{C}^n$ . Writing $z=u+iv$ with $u,v\in\mathbb{R}^n$ , symmetry gives $z^*Mz=u^{\mathsf T}Mu+v^{\mathsf T}Mv$ , and at least one of $u,v$ is nonzero.

Preamble

import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef

open scoped ComplexOrder

Formal statement

theorem Matrix.PosDef.map_ofReal {n : Type*} [Fintype n] {M : Matrix n n ℝ} (hM : M.PosDef) :
    (M.map (fun x : ℝ => (x : ℂ))).PosDef := by sorry

Source

Standard linear algebra (complexification of a real inner product).

View graph

A real positive definite matrix is positive definite over C\mathbb{C}C

A real positive definite matrix is positive definite over $\mathbb{C}$