Metamath Proof Explorer

Table of Contents - 11.3.1. Definition and basic properties

  1. cmps
  2. cmvr
  3. cmpl
  4. cltb
  5. copws
  6. df-psr
  7. df-mvr
  8. df-mpl
  9. df-ltbag
  10. df-opsr
  11. reldmpsr
  12. psrval
  13. psrvalstr
  14. psrbag
  15. psrbagf
  16. psrbagfsupp
  17. snifpsrbag
  18. fczpsrbag
  19. psrbaglesupp
  20. psrbaglecl
  21. psrbagaddcl
  22. psrbagcon
  23. psrbaglefi
  24. psrbagconcl
  25. psrbagleadd1
  26. psrbagconf1o
  27. gsumbagdiaglem
  28. gsumbagdiag
  29. psrass1lem
  30. psrbas
  31. psrelbas
  32. psrelbasfun
  33. psrplusg
  34. psradd
  35. psraddcl
  36. psraddclOLD
  37. rhmpsrlem1
  38. rhmpsrlem2
  39. psrmulr
  40. psrmulfval
  41. psrmulval
  42. psrmulcllem
  43. psrmulcl
  44. psrsca
  45. psrvscafval
  46. psrvsca
  47. psrvscaval
  48. psrvscacl
  49. psr0cl
  50. psr0lid
  51. psrnegcl
  52. psrlinv
  53. psrgrp
  54. psr0
  55. psrneg
  56. psrlmod
  57. psr1cl
  58. psrlidm
  59. psrridm
  60. psrass1
  61. psrdi
  62. psrdir
  63. psrass23l
  64. psrcom
  65. psrass23
  66. psrring
  67. psr1
  68. psrcrng
  69. psrassa
  70. resspsrbas
  71. resspsradd
  72. resspsrmul
  73. resspsrvsca
  74. subrgpsr
  75. psrascl
  76. psrasclcl
  77. mvrfval
  78. mvrval
  79. mvrval2
  80. mvrid
  81. mvrf
  82. mvrf1
  83. mvrcl2
  84. reldmmpl
  85. mplval
  86. mplbas
  87. mplelbas
  88. mvrcl
  89. mvrf2
  90. mplrcl
  91. mplelsfi
  92. mplval2
  93. mplbasss
  94. mplelf
  95. mplsubglem
  96. mpllsslem
  97. mplsubglem2
  98. mplsubg
  99. mpllss
  100. mplsubrglem
  101. mplsubrg
  102. mpl0
  103. mplplusg
  104. mplmulr
  105. mpladd
  106. mplneg
  107. mplmul
  108. mpl1
  109. mplsca
  110. mplvsca2
  111. mplvsca
  112. mplvscaval
  113. mplgrp
  114. mpllmod
  115. mplring
  116. mpllvec
  117. mplcrng
  118. mplassa
  119. mplringd
  120. mpllmodd
  121. mplascl0
  122. mplascl1
  123. ressmplbas2
  124. ressmplbas
  125. ressmpladd
  126. ressmplmul
  127. ressmplvsca
  128. subrgmpl
  129. subrgmvr
  130. subrgmvrf
  131. mplmon
  132. mplmonmul
  133. mplcoe1
  134. mplcoe3
  135. mplcoe5lem
  136. mplcoe5
  137. mplcoe2
  138. mplbas2
  139. ltbval
  140. ltbwe
  141. reldmopsr
  142. opsrval
  143. opsrle
  144. opsrval2
  145. opsrbaslem
  146. opsrbas
  147. opsrplusg
  148. opsrmulr
  149. opsrvsca
  150. opsrsca
  151. opsrtoslem1
  152. opsrtoslem2
  153. opsrtos
  154. opsrso
  155. opsrcrng
  156. opsrassa
  157. mplmon2
  158. psrbag0
  159. psrbagsn
  160. mplascl
  161. mplasclf
  162. subrgascl
  163. subrgasclcl
  164. mplmon2cl
  165. mplmon2mul
  166. mplind
  167. mplcoe4