OAI/Analysis/Commutator/StableScalarGeometry.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.Decomposable.evalL_indicatorline 26 - lemma
OAI.Kadison.Decomposable.vector_indicator_of_scalarline 46 - lemma
OAI.Kadison.Decomposable.scalarVectorMultiplier_commutes_constantline 59