Metamath Proof Explorer
Table of Contents - 11.2.1. Definition and basic properties
- casa
- casp
- cascl
- df-assa
- df-asp
- df-ascl
- isassa
- assalem
- assaass
- assaassr
- assalmod
- assaring
- assasca
- assa2ass
- isassad
- issubassa3
- issubassa
- sraassa
- rlmassa
- assapropd
- aspval
- asplss
- aspid
- aspsubrg
- aspss
- aspssid
- asclfval
- asclval
- asclfn
- asclf
- asclghm
- ascl0
- ascl1
- asclmul1
- asclmul2
- ascldimul
- asclinvg
- asclrhm
- rnascl
- issubassa2
- rnasclsubrg
- rnasclmulcl
- rnasclassa
- ressascl
- asclpropd
- aspval2
- assamulgscmlem1
- assamulgscmlem2
- assamulgscm
- zlmassa