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