Metamath Proof Explorer

Table of Contents - 21.3.9. Algebra

1. Monoids
   1. cmn4d
   2. cmn246135
   3. cmn145236
   4. submcld
2. Monoids Homomorphisms
   1. abliso
   2. lmhmghmd
   3. mhmimasplusg
   4. lmhmimasvsca
3. 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
4. Centralizers and centers - misc additions
   1. cntzun
   2. cntzsnid
   3. cntrcrng
5. 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
6. The symmetric group
   1. symgfcoeu
   2. symgcom
   3. symgcom2
   4. symgcntz
   5. odpmco
   6. symgsubg
   7. pmtrprfv2
   8. pmtrcnel
   9. pmtrcnel2
   10. pmtrcnelor
7. Transpositions
   1. pmtridf1o
   2. pmtridfv1
   3. pmtridfv2
8. Permutation Signs
   1. psgnid
   2. psgndmfi
   3. pmtrto1cl
   4. psgnfzto1stlem
   5. fzto1stfv1
   6. fzto1st1
   7. fzto1st
   8. fzto1stinvn
   9. psgnfzto1st
9. 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
10. 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
11. Signum in an ordered monoid
    1. csgns
    2. df-sgns
    3. sgnsv
    4. sgnsval
    5. sgnsf
12. 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
13. 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
14. Simple groups
    1. prmsimpcyc
15. Rings - misc additions
    1. cringmul32d
    2. ringdid
    3. ringdird
    4. urpropd
    5. frobrhm
    6. ress1r
    7. ringinvval
    8. dvrcan5
    9. subrgchr
    10. rmfsupp2
    11. unitnz
16. The zero ring
    1. irrednzr
    2. 0ringsubrg
    3. 0ringcring
17. Localization of rings
    1. cerl
    2. crloc
    3. df-erl
    4. df-rloc
    5. reldmrloc
    6. erlval
    7. rlocval
    8. erlcl1
    9. erlcl2
    10. erldi
    11. erlbrd
    12. erlbr2d
    13. erler
    14. elrlocbasi
    15. rlocbas
    16. rlocaddval
    17. rlocmulval
    18. rloccring
    19. rloc0g
    20. rloc1r
    21. rlocf1
18. Integral Domains
    1. domnlcan
    2. idomrcan
    3. 1rrg
    4. rrgnz
    5. isdomn6
    6. rrgsubm
    7. subrdom
    8. subridom
    9. subrfld
19. Euclidean Domains
    1. ceuf
    2. df-euf
    3. eufndx
    4. eufid
    5. cedom
    6. df-edom
20. Division Rings
    1. ringinveu
    2. isdrng4
    3. rndrhmcl
21. Subfields
    1. sdrgdvcl
    2. sdrginvcl
    3. primefldchr
22. Field of fractions
    1. cfrac
    2. df-frac
    3. fracval
    4. fracbas
    5. fracerl
    6. fracf1
    7. fracfld
    8. idomsubr
23. Field extensions generated by a set
    1. cfldgen
    2. df-fldgen
    3. fldgenval
    4. fldgenssid
    5. fldgensdrg
    6. fldgenssv
    7. fldgenss
    8. fldgenidfld
    9. fldgenssp
    10. fldgenid
    11. fldgenfld
    12. primefldgen1
    13. 1fldgenq
24. 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
25. Ring homomorphisms - misc additions
    1. rhmdvd
    2. kerunit
26. 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
27. The commutative ring of gaussian integers
    1. gzcrng
28. The archimedean ordered field of real numbers
    1. reofld
    2. nn0omnd
    3. rearchi
    4. nn0archi
    5. xrge0slmod
29. The quotient map and quotient modules
    1. qusker
    2. eqgvscpbl
    3. qusvscpbl
    4. qusvsval
    5. imaslmod
    6. imasmhm
    7. imasghm
    8. imasrhm
    9. imaslmhm
    10. quslmod
    11. quslmhm
    12. quslvec
    13. ecxpid
    14. qsxpid
    15. qusxpid
    16. qustriv
    17. qustrivr
30. The ring of integers modulo ` N `
    1. znfermltl
31. Independent sets and families
    1. islinds5
    2. ellspds
    3. 0ellsp
    4. 0nellinds
    5. rspsnel
    6. rspsnid
    7. elrsp
    8. ellpi
    9. rspidlid
    10. pidlnz
    11. dvdsruassoi
    12. dvdsruasso
    13. dvdsruasso2
    14. dvdsrspss
    15. rspsnasso
    16. lbslsp
    17. lindssn
    18. lindflbs
    19. islbs5
    20. linds2eq
    21. lindfpropd
    22. lindspropd
32. 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
33. The quotient map
    1. qusmul
    2. quslsm
    3. qusbas2
    4. qus0g
    5. qusima
    6. qusrn
    7. nsgqus0
    8. nsgmgclem
    9. nsgmgc
    10. nsgqusf1olem1
    11. nsgqusf1olem2
    12. nsgqusf1olem3
    13. nsgqusf1o
    14. lmhmqusker
    15. lmicqusker
    16. ghmqusnsglem1
    17. ghmqusnsglem2
    18. ghmqusnsg
34. Ideals
    1. intlidl
    2. rhmpreimaidl
    3. kerlidl
    4. lidlnsg
    5. 0ringidl
    6. pidlnzb
    7. lidlunitel
    8. unitpidl1
    9. rhmquskerlem
    10. rhmqusker
    11. ricqusker
    12. rhmqusnsg
    13. elrspunidl
    14. elrspunsn
    15. lidlincl
    16. idlinsubrg
    17. rhmimaidl
    18. drngidl
    19. drngidlhash
35. 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. cringm4
    13. isprmidlc
    14. prmidlc
    15. 0ringprmidl
    16. prmidl0
    17. rhmpreimaprmidl
    18. qsidomlem1
    19. qsidomlem2
    20. qsidom
    21. qsnzr
36. Maximal Ideals
    1. cmxidl
    2. df-mxidl
    3. mxidlval
    4. ismxidl
    5. mxidlidl
    6. mxidlnr
    7. mxidlmax
    8. mxidln1
    9. mxidlnzr
    10. mxidlmaxv
    11. crngmxidl
    12. mxidlprm
    13. mxidlirredi
    14. mxidlirred
    15. ssmxidllem
    16. ssmxidl
    17. drnglidl1ne0
    18. drng0mxidl
    19. drngmxidl
    20. krull
    21. mxidlnzrb
    22. opprabs
    23. oppreqg
    24. opprnsg
    25. opprlidlabs
    26. oppr2idl
    27. opprmxidlabs
    28. opprqusbas
    29. opprqusplusg
    30. opprqus0g
    31. opprqusmulr
    32. opprqus1r
    33. opprqusdrng
    34. qsdrngilem
    35. qsdrngi
    36. qsdrnglem2
    37. qsdrng
    38. qsfld
    39. mxidlprmALT
37. 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
38. Prime Elements
    1. rprmval
    2. isrprm
    3. rprmcl
    4. rprmdvds
    5. rprmnz
    6. rprmnunit
    7. rsprprmprmidl
    8. rsprprmprmidlb
    9. rprmndvdsr1
    10. rprmasso
    11. rprmasso2
    12. rprmirredlem
    13. rprmirred
    14. rprmirredb
    15. rprmdvdspow
    16. rprmdvdsprod
39. Unique factorization domains
    1. cufd
    2. df-ufd
    3. isufd
    4. isufd2
    5. ufdcringd
    6. 0ringufd
40. The ring of integers
    1. zringidom
    2. zringpid
    3. dfprm3
    4. zringfrac
41. Univariate Polynomials
    1. 0ringmon1p
    2. fply1
    3. ply1lvec
    4. evls1fn
    5. evls1dm
    6. evls1fvf
    7. ressdeg1
    8. ressply10g
    9. ressply1mon1p
    10. ressply1invg
    11. ressply1sub
    12. evls1subd
    13. ply1ascl1
    14. deg1le0eq0
    15. ply1asclunit
    16. ply1unit
    17. m1pmeq
    18. ply1fermltl
    19. coe1mon
    20. ply1moneq
    21. ply1degltel
    22. ply1degleel
    23. ply1degltlss
    24. gsummoncoe1fzo
    25. ply1gsumz
    26. deg1addlt
    27. ig1pnunit
    28. ig1pmindeg
42. Polynomial quotient and polynomial remainder
    1. q1pdir
    2. q1pvsca
    3. r1pvsca
    4. r1p0
    5. r1pcyc
    6. r1padd1
    7. r1pid2
    8. r1plmhm
    9. r1pquslmic
43. The subring algebra
    1. sra1r
    2. sradrng
    3. srasubrg
    4. sralvec
    5. srafldlvec
    6. resssra
    7. lsssra
44. Division Ring Extensions
    1. drgext0g
    2. drgextvsca
    3. drgext0gsca
    4. drgextsubrg
    5. drgextlsp
    6. drgextgsum
45. Vector Spaces
    1. lvecdimfi
46. Vector Space Dimension
    1. cldim
    2. df-dim
    3. dimval
    4. dimvalfi
    5. dimcl
    6. lmimdim
    7. lmicdim
    8. lvecdim0i
    9. lvecdim0
    10. lssdimle
    11. dimpropd
    12. rlmdim
    13. rgmoddimOLD
    14. frlmdim
    15. tnglvec
    16. tngdim
    17. rrxdim
    18. matdim
    19. lbslsat
    20. lsatdim
    21. drngdimgt0
    22. lmhmlvec2
    23. kerlmhm
    24. imlmhm
    25. ply1degltdimlem
    26. ply1degltdim
    27. lindsunlem
    28. lindsun
    29. lbsdiflsp0
    30. dimkerim
    31. qusdimsum
    32. fedgmullem1
    33. fedgmullem2
    34. fedgmul