Metamath Proof Explorer

Table of Contents - 20.43.20. Basic algebraic structures (extension)

1. Auxiliary theorems
   1. opeliun2xp
   2. eliunxp2
   3. mpomptx2
   4. cbvmpox2
   5. dmmpossx2
   6. mpoexxg2
   7. ovmpordxf
   8. ovmpordx
   9. ovmpox2
   10. fdmdifeqresdif
   11. offvalfv
   12. ofaddmndmap
   13. mapsnop
   14. fprmappr
   15. mapprop
   16. ztprmneprm
   17. 2t6m3t4e0
   18. ssnn0ssfz
   19. nn0sumltlt
2. The binomial coefficient operation (extension)
   1. bcpascm1
   2. altgsumbc
   3. altgsumbcALT
3. The ` ZZ `-module ` ZZ X. ZZ `
   1. zlmodzxzlmod
   2. zlmodzxzel
   3. zlmodzxz0
   4. zlmodzxzscm
   5. zlmodzxzadd
   6. zlmodzxzsubm
   7. zlmodzxzsub
4. Group sum operation (extension 2)
   1. mgpsumunsn
   2. mgpsumz
   3. mgpsumn
5. Symmetric groups (extension)
   1. exple2lt6
   2. pgrple2abl
   3. pgrpgt2nabl
6. Divisibility (extension)
   1. invginvrid
7. The support of functions (extension)
   1. rmsupp0
   2. domnmsuppn0
   3. rmsuppss
   4. mndpsuppss
   5. scmsuppss
8. Finitely supported functions (extension)
   1. rmsuppfi
   2. rmfsupp
   3. mndpsuppfi
   4. mndpfsupp
   5. scmsuppfi
   6. scmfsupp
   7. suppmptcfin
   8. mptcfsupp
   9. fsuppmptdmf
9. Left modules (extension)
   1. lmodvsmdi
   2. gsumlsscl
10. Associative algebras (extension)
    1. ascl1
    2. assaascl0
    3. assaascl1
11. Univariate polynomials (extension)
    1. ply1vr1smo
    2. ply1ass23l
    3. ply1sclrmsm
    4. coe1id
    5. coe1sclmulval
    6. ply1mulgsumlem1
    7. ply1mulgsumlem2
    8. ply1mulgsumlem3
    9. ply1mulgsumlem4
    10. ply1mulgsum
    11. evl1at0
    12. evl1at1
12. Univariate polynomials (examples)
    1. linply1
    2. lineval
    3. linevalexample