OAI/Analysis/Commutator/ModuleZeroExtension.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.ReducingRepresentation.project_intertwines line 28
2. def OAI.Kadison.ReducingRepresentation.extendZero line 36
3. lemma OAI.Kadison.ReducingRepresentation.extendZero_subtype line 39
4. lemma OAI.Kadison.ReducingRepresentation.extendZero_intertwines line 43
5. lemma OAI.Kadison.ReducingRepresentation.norm_sub_extendZero_apply_le line 52