OAI/Analysis/Commutator/KaplanskyRange.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Kadison.Kaplansky.selfAdjoint_contraction_finite_approx_of_clipline 23 - lemma
OAI.Kadison.Kaplansky.clip_mem_rangeline 56 - theorem
OAI.Kadison.Kaplansky.range_selfAdjoint_contraction_finite_approxline 69