Registry · Proposition IV.P17 tau-effective formalized

IV.P17 — Inner Product Properties

Sesquilinear, Hermitian, positive definite. Positive definiteness uses CR identity theorem.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (1)

IV.D61

Depended on by (1)

IV.D62

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.InnerProductProperties