Namespace `LinearAlgebra` 1 theorems

Eigenvector plus image decomposition for a sum of squares of skew operators LinearAlgebra.exists_eigenvector_add_image_sum_sq_of_skew_of_posDef_hermitian 0 below · cited by 1 · depth 38

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.

Namespace LinearAlgebra 1 theorems

Namespace `LinearAlgebra` 1 theorems