OAI/Analysis/JiangSu/CentralSequences/NormTraceKernelSigma.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NonunitalGamma.kernel_diagonal_choice line 22
2. lemma OAI.NonunitalGamma.eventually_norm_lt_of_quotient_norm_lt line 42
3. theorem OAI.NonunitalGamma.trace_kernel_sigma_ideal line 48
4. theorem OAI.NonunitalGamma.normToTracial_central_surjective line 143
5. theorem OAI.NonunitalGamma.exists_norm_central_local_unit line 175