Metamath Proof Explorer

Table of Contents - 20.3.9. Algebra

1. Monoids Homomorphisms
   1. abliso
2. Finitely supported group sums - misc additions
   1. gsumsubg
   2. gsumsra
   3. gsummpt2co
   4. gsummpt2d
   5. lmodvslmhm
   6. gsumvsmul1
   7. gsummptres
   8. gsummptres2
   9. gsumzresunsn
   10. gsumpart
   11. gsumhashmul
   12. xrge0tsmsd
   13. xrge0tsmsbi
   14. xrge0tsmseq
3. Centralizers and centers - misc additions
   1. cntzun
   2. cntzsnid
   3. cntrcrng
4. Totally ordered monoids and groups
   1. comnd
   2. cogrp
   3. df-omnd
   4. df-ogrp
   5. isomnd
   6. isogrp
   7. ogrpgrp
   8. omndmnd
   9. omndtos
   10. omndadd
   11. omndaddr
   12. omndadd2d
   13. omndadd2rd
   14. submomnd
   15. xrge0omnd
   16. omndmul2
   17. omndmul3
   18. omndmul
   19. ogrpinv0le
   20. ogrpsub
   21. ogrpaddlt
   22. ogrpaddltbi
   23. ogrpaddltrd
   24. ogrpaddltrbid
   25. ogrpsublt
   26. ogrpinv0lt
   27. ogrpinvlt
   28. gsumle
5. The symmetric group
   1. symgfcoeu
   2. symgcom
   3. symgcom2
   4. symgcntz
   5. odpmco
   6. symgsubg
   7. pmtrprfv2
   8. pmtrcnel
   9. pmtrcnel2
   10. pmtrcnelor
6. Transpositions
   1. pmtridf1o
   2. pmtridfv1
   3. pmtridfv2
7. Permutation Signs
   1. psgnid
   2. psgndmfi
   3. pmtrto1cl
   4. psgnfzto1stlem
   5. fzto1stfv1
   6. fzto1st1
   7. fzto1st
   8. fzto1stinvn
   9. psgnfzto1st
8. Permutation cycles
   1. ctocyc
   2. df-tocyc
   3. tocycval
   4. tocycfv
   5. tocycfvres1
   6. tocycfvres2
   7. cycpmfvlem
   8. cycpmfv1
   9. cycpmfv2
   10. cycpmfv3
   11. cycpmcl
   12. tocycf
   13. tocyc01
   14. cycpm2tr
   15. cycpm2cl
   16. cyc2fv1
   17. cyc2fv2
   18. trsp2cyc
   19. cycpmco2f1
   20. cycpmco2rn
   21. cycpmco2lem1
   22. cycpmco2lem2
   23. cycpmco2lem3
   24. cycpmco2lem4
   25. cycpmco2lem5
   26. cycpmco2lem6
   27. cycpmco2lem7
   28. cycpmco2
   29. cyc2fvx
   30. cycpm3cl
   31. cycpm3cl2
   32. cyc3fv1
   33. cyc3fv2
   34. cyc3fv3
   35. cyc3co2
   36. cycpmconjvlem
   37. cycpmconjv
   38. cycpmrn
   39. tocyccntz
9. The Alternating Group
   1. evpmval
   2. cnmsgn0g
   3. evpmsubg
   4. evpmid
   5. altgnsg
   6. cyc3evpm
   7. cyc3genpmlem
   8. cyc3genpm
   9. cycpmgcl
   10. cycpmconjslem1
   11. cycpmconjslem2
   12. cycpmconjs
   13. cyc3conja
10. Signum in an ordered monoid
    1. csgns
    2. df-sgns
    3. sgnsv
    4. sgnsval
    5. sgnsf
11. The Archimedean property for generic ordered algebraic structures
    1. cinftm
    2. carchi
    3. df-inftm
    4. df-archi
    5. inftmrel
    6. isinftm
    7. isarchi
    8. pnfinf
    9. xrnarchi
    10. isarchi2
    11. submarchi
    12. isarchi3
    13. archirng
    14. archirngz
    15. archiexdiv
    16. archiabllem1a
    17. archiabllem1b
    18. archiabllem1
    19. archiabllem2a
    20. archiabllem2c
    21. archiabllem2b
    22. archiabllem2
    23. archiabl
12. Semiring left modules
    1. cslmd
    2. df-slmd
    3. isslmd
    4. slmdlema
    5. lmodslmd
    6. slmdcmn
    7. slmdmnd
    8. slmdsrg
    9. slmdbn0
    10. slmdacl
    11. slmdmcl
    12. slmdsn0
    13. slmdvacl
    14. slmdass
    15. slmdvscl
    16. slmdvsdi
    17. slmdvsdir
    18. slmdvsass
    19. slmd0cl
    20. slmd1cl
    21. slmdvs1
    22. slmd0vcl
    23. slmd0vlid
    24. slmd0vrid
    25. slmd0vs
    26. slmdvs0
    27. gsumvsca1
    28. gsumvsca2
13. Simple groups
    1. prmsimpcyc
14. Rings - misc additions
    1. rngurd
    2. dvdschrmulg
    3. freshmansdream
    4. frobrhm
    5. ress1r
    6. dvrdir
    7. rdivmuldivd
    8. ringinvval
    9. dvrcan5
    10. subrgchr
    11. rmfsupp2
15. Subfields
    1. primefldchr
16. Totally ordered rings and fields
    1. corng
    2. cofld
    3. df-orng
    4. df-ofld
    5. isorng
    6. orngring
    7. orngogrp
    8. isofld
    9. orngmul
    10. orngsqr
    11. ornglmulle
    12. orngrmulle
    13. ornglmullt
    14. orngrmullt
    15. orngmullt
    16. ofldfld
    17. ofldtos
    18. orng0le1
    19. ofldlt1
    20. ofldchr
    21. suborng
    22. subofld
    23. isarchiofld
17. Ring homomorphisms - misc additions
    1. rhmdvdsr
    2. rhmopp
    3. elrhmunit
    4. rhmdvd
    5. rhmunitinv
    6. kerunit
18. Scalar restriction operation
    1. cresv
    2. df-resv
    3. reldmresv
    4. resvval
    5. resvid2
    6. resvval2
    7. resvsca
    8. resvlem
    9. resvlemOLD
    10. resvbas
    11. resvbasOLD
    12. resvplusg
    13. resvplusgOLD
    14. resvvsca
    15. resvvscaOLD
    16. resvmulr
    17. resvmulrOLD
    18. resv0g
    19. resv1r
    20. resvcmn
19. The commutative ring of gaussian integers
    1. gzcrng
20. The archimedean ordered field of real numbers
    1. reofld
    2. nn0omnd
    3. rearchi
    4. nn0archi
    5. xrge0slmod
21. The quotient map and quotient modules
    1. qusker
    2. eqgvscpbl
    3. qusvscpbl
    4. qusscaval
    5. imaslmod
    6. quslmod
    7. quslmhm
    8. ecxpid
    9. eqg0el
    10. qsxpid
    11. qusxpid
    12. qustriv
    13. qustrivr
22. The ring of integers modulo ` N `
    1. znfermltl
23. Independent sets and families
    1. islinds5
    2. ellspds
    3. 0ellsp
    4. 0nellinds
    5. rspsnel
    6. rspsnid
    7. elrsp
    8. rspidlid
    9. pidlnz
    10. lbslsp
    11. lindssn
    12. lindflbs
    13. linds2eq
    14. lindfpropd
    15. lindspropd
24. Subgroup sum / Sumset / Minkowski sum
    1. elgrplsmsn
    2. lsmsnorb
    3. lsmsnorb2
    4. elringlsm
    5. elringlsmd
    6. ringlsmss
    7. ringlsmss1
    8. ringlsmss2
    9. lsmsnpridl
    10. lsmsnidl
    11. lsmidllsp
    12. lsmidl
    13. lsmssass
    14. grplsm0l
    15. grplsmid
25. The quotient map
    1. quslsm
    2. qusima
    3. nsgqus0
    4. nsgmgclem
    5. nsgmgc
    6. nsgqusf1olem1
    7. nsgqusf1olem2
    8. nsgqusf1olem3
    9. nsgqusf1o
26. Ideals
    1. intlidl
    2. rhmpreimaidl
    3. kerlidl
    4. 0ringidl
    5. elrspunidl
    6. lidlincl
    7. idlinsubrg
    8. rhmimaidl
27. Prime Ideals
    1. cprmidl
    2. df-prmidl
    3. prmidlval
    4. isprmidl
    5. prmidlnr
    6. prmidl
    7. prmidl2
    8. idlmulssprm
    9. pridln1
    10. prmidlidl
    11. prmidlssidl
    12. lidlnsg
    13. cringm4
    14. isprmidlc
    15. prmidlc
    16. 0ringprmidl
    17. prmidl0
    18. rhmpreimaprmidl
    19. qsidomlem1
    20. qsidomlem2
    21. qsidom
28. Maximal Ideals
    1. cmxidl
    2. df-mxidl
    3. mxidlval
    4. ismxidl
    5. mxidlidl
    6. mxidlnr
    7. mxidlmax
    8. mxidln1
    9. mxidlnzr
    10. mxidlprm
    11. ssmxidllem
    12. ssmxidl
    13. krull
    14. mxidlnzrb
29. The semiring of ideals of a ring
    1. cidlsrg
    2. df-idlsrg
    3. idlsrgstr
    4. idlsrgval
    5. idlsrgbas
    6. idlsrgplusg
    7. idlsrg0g
    8. idlsrgmulr
    9. idlsrgtset
    10. idlsrgmulrval
    11. idlsrgmulrcl
    12. idlsrgmulrss1
    13. idlsrgmulrss2
    14. idlsrgmulrssin
    15. idlsrgmnd
    16. idlsrgcmnd
30. Prime Elements
31. Unique factorization domains
    1. cufd
    2. df-ufd
    3. isufd
    4. rprmval
    5. isrprm
32. Associative algebras
    1. asclmulg
33. Univariate Polynomials
    1. fply1
    2. ply1scleq
    3. ply1chr
    4. ply1fermltl
34. The subring algebra
    1. sra1r
    2. sraring
    3. sradrng
    4. srasubrg
    5. sralvec
    6. srafldlvec
35. Division Ring Extensions
    1. drgext0g
    2. drgextvsca
    3. drgext0gsca
    4. drgextsubrg
    5. drgextlsp
    6. drgextgsum
36. Vector Spaces
    1. lvecdimfi
37. Vector Space Dimension
    1. cldim
    2. df-dim
    3. dimval
    4. dimvalfi
    5. dimcl
    6. lvecdim0i
    7. lvecdim0
    8. lssdimle
    9. dimpropd
    10. rgmoddim
    11. frlmdim
    12. tnglvec
    13. tngdim
    14. rrxdim
    15. matdim
    16. lbslsat
    17. lsatdim
    18. drngdimgt0
    19. lmhmlvec2
    20. kerlmhm
    21. imlmhm
    22. lindsunlem
    23. lindsun
    24. lbsdiflsp0
    25. dimkerim
    26. qusdimsum
    27. fedgmullem1
    28. fedgmullem2
    29. fedgmul