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. zringsubgval
    4. linevalexample