Metamath Proof Explorer
Table of Contents - 11.3.1. Definition and basic properties
- cmps
- cmvr
- cmpl
- cltb
- copws
- df-psr
- df-mvr
- df-mpl
- df-ltbag
- df-opsr
- reldmpsr
- psrval
- psrvalstr
- psrbag
- psrbagf
- psrbagfOLD
- psrbagfsupp
- psrbagfsuppOLD
- snifpsrbag
- fczpsrbag
- psrbaglesupp
- psrbaglesuppOLD
- psrbaglecl
- psrbagleclOLD
- psrbagaddcl
- psrbagaddclOLD
- psrbagcon
- psrbagconOLD
- psrbaglefi
- psrbaglefiOLD
- psrbagconcl
- psrbagconclOLD
- psrbagconf1o
- psrbagconf1oOLD
- gsumbagdiaglemOLD
- gsumbagdiagOLD
- psrass1lemOLD
- gsumbagdiaglem
- gsumbagdiag
- psrass1lem
- psrbas
- psrelbas
- psrelbasfun
- psrplusg
- psradd
- psraddcl
- psrmulr
- psrmulfval
- psrmulval
- psrmulcllem
- psrmulcl
- psrsca
- psrvscafval
- psrvsca
- psrvscaval
- psrvscacl
- psr0cl
- psr0lid
- psrnegcl
- psrlinv
- psrgrp
- psr0
- psrneg
- psrlmod
- psr1cl
- psrlidm
- psrridm
- psrass1
- psrdi
- psrdir
- psrass23l
- psrcom
- psrass23
- psrring
- psr1
- psrcrng
- psrassa
- resspsrbas
- resspsradd
- resspsrmul
- resspsrvsca
- subrgpsr
- mvrfval
- mvrval
- mvrval2
- mvrid
- mvrf
- mvrf1
- mvrcl2
- reldmmpl
- mplval
- mplbas
- mplelbas
- mplrcl
- mplelsfi
- mplval2
- mplbasss
- mplelf
- mplsubglem
- mpllsslem
- mplsubglem2
- mplsubg
- mpllss
- mplsubrglem
- mplsubrg
- mpl0
- mpladd
- mplneg
- mplmul
- mpl1
- mplsca
- mplvsca2
- mplvsca
- mplvscaval
- mvrcl
- mplgrp
- mpllmod
- mplring
- mpllvec
- mplcrng
- mplassa
- ressmplbas2
- ressmplbas
- ressmpladd
- ressmplmul
- ressmplvsca
- subrgmpl
- subrgmvr
- subrgmvrf
- mplmon
- mplmonmul
- mplcoe1
- mplcoe3
- mplcoe5lem
- mplcoe5
- mplcoe2
- mplbas2
- ltbval
- ltbwe
- reldmopsr
- opsrval
- opsrle
- opsrval2
- opsrbaslem
- opsrbaslemOLD
- opsrbas
- opsrbasOLD
- opsrplusg
- opsrplusgOLD
- opsrmulr
- opsrmulrOLD
- opsrvsca
- opsrvscaOLD
- opsrsca
- opsrscaOLD
- opsrtoslem1
- opsrtoslem2
- opsrtos
- opsrso
- opsrcrng
- opsrassa
- mvrf2
- mplmon2
- psrbag0
- psrbagsn
- mplascl
- mplasclf
- subrgascl
- subrgasclcl
- mplmon2cl
- mplmon2mul
- mplind
- mplcoe4