OAI/Analysis/CharacterCriterion/SeparableReduction.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KirchbergRordam.GenericRW.SeparableReduction.stage line 35
2. lemma OAI.KirchbergRordam.GenericRW.SeparableReduction.stage_step line 39
3. lemma OAI.KirchbergRordam.GenericRW.SeparableReduction.stage_mono line 41
4. lemma OAI.KirchbergRordam.GenericRW.SeparableReduction.stage_separable line 42
5. def OAI.KirchbergRordam.GenericRW.SeparableReduction.termAlgebra line 47
6. lemma OAI.KirchbergRordam.GenericRW.SeparableReduction.adjoin_separable line 68
7. lemma OAI.KirchbergRordam.GenericRW.SeparableReduction.closedAdjoin_separable line 75
8. abbrev OAI.KirchbergRordam.GenericRW.SeparableReduction.Term line 82
9. def OAI.KirchbergRordam.GenericRW.SeparableReduction.term line 83
10. lemma OAI.KirchbergRordam.GenericRW.SeparableReduction.span_commutator_list line 84
11. theorem OAI.KirchbergRordam.GenericRW.separable_characterless_subalgebra line 124
12. theorem OAI.KirchbergRordam.GenericRW.MaxTensor.separable_maxTensor line 174
13. instance OAI.KirchbergRordam.GenericRW.MaxTensor.powerPack_separable line 198
14. lemma OAI.KirchbergRordam.PrimeDimensionDrop.eval_apply line 212
15. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 216) line 216
16. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 218) line 218
17. def OAI.KirchbergRordam.PrimeDimensionDrop.inclusion line 220
18. def OAI.KirchbergRordam.PrimeDimensionDrop.evaluation line 223
19. lemma OAI.KirchbergRordam.PrimeDimensionDrop.evaluation_apply line 226
20. lemma OAI.KirchbergRordam.PrimeDimensionDrop.mem_iff line 229
21. lemma OAI.KirchbergRordam.PrimeDimensionDrop.norm_le_iff line 235
22. def OAI.KirchbergRordam.PrimeDimensionDrop.scalar line 240
23. def OAI.KirchbergRordam.PrimeDimensionDrop.reparam line 253
24. theorem OAI.KirchbergRordam.NormUltrapower.generic_maximal_power_to_central line 271
25. theorem OAI.KirchbergRordam.central_prime_power_drop line 289