Metamath Proof Explorer

Table of Contents - 21.25.20. Ideals

1. cidl
2. cpridl
3. cmaxidl
4. df-idl
5. df-pridl
6. df-maxidl
7. idlval
8. isidl
9. isidlc
10. idlss
11. idlcl
12. idl0cl
13. idladdcl
14. idllmulcl
15. idlrmulcl
16. idlnegcl
17. idlsubcl
18. rngoidl
19. 0idl
20. 1idl
21. 0rngo
22. divrngidl
23. intidl
24. inidl
25. unichnidl
26. keridl
27. pridlval
28. ispridl
29. pridlidl
30. pridlnr
31. pridl
32. ispridl2
33. maxidlval
34. ismaxidl
35. maxidlidl
36. maxidlnr
37. maxidlmax
38. maxidln1
39. maxidln0