OAI/Analysis/JiangSu/Nonunital/ClosedIdealBasic.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.NonunitalClosedIdeal.Ideal line 14
2. instance OAI.NonunitalClosedIdeal.(instance at line 22) line 22
3. def OAI.NonunitalClosedIdeal.ringCon line 24
4. def OAI.NonunitalClosedIdeal.QuotientAlgebra line 37
5. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 39) line 39
6. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 41) line 41
7. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 43) line 43
8. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 45) line 45
9. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 47) line 47
10. def OAI.NonunitalClosedIdeal.QuotientAlgebra.mk line 50
11. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.mk_add line 51
12. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.mk_mul line 52
13. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.mk_sub line 53
14. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.mk_smul line 54
15. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.mk_zero line 55
16. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.mk_surjective line 56
17. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.mk_eq_mk_iff line 57
18. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.norm_mk_le line 59
19. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.exists_norm_mk_lt line 60
20. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 63) line 63
21. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 77) line 77
22. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.mk_star line 83
23. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 84) line 84
24. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 99) line 99
25. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 104) line 104
26. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 110) line 110
27. def OAI.NonunitalClosedIdeal.QuotientAlgebra.mkHom line 117
28. def OAI.NonunitalClosedIdeal.idealStarAlgebra line 140
29. instance OAI.NonunitalClosedIdeal.(instance at line 148) line 148
30. instance OAI.NonunitalClosedIdeal.(instance at line 149) line 149
31. instance OAI.NonunitalClosedIdeal.(instance at line 151) line 151
32. instance OAI.NonunitalClosedIdeal.(instance at line 152) line 152
33. def OAI.NonunitalClosedIdeal.idealInclusion line 154
34. lemma OAI.NonunitalClosedIdeal.exists_ideal_contraction line 162
35. lemma OAI.NonunitalClosedIdeal.QuotientAlgebra.quotient_norm_square_le line 184
36. instance OAI.NonunitalClosedIdeal.QuotientAlgebra.(instance at line 230) line 230