OAI/Analysis/Commutator/FactorMetric.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.CbFactor.gram_strictlyPositiveline 19 - lemma
OAI.Kadison.CbFactor.gram_intertwinesline 51
OAI/Analysis/Commutator/FactorMetric.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.Kadison.CbFactor.gram_strictlyPositive line 19OAI.Kadison.CbFactor.gram_intertwines line 51