OAI/Analysis/KadisonKastler/HermitianLinearExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Complexification of self-adjoint pairing identities

  1. theorem OAI.KadisonKastler.complexLinear_eq_of_selfAdjoint line 14
  2. theorem OAI.KadisonKastler.hermitianLinear_eq_of_selfAdjoint_real line 20