Metamath Proof Explorer

Table of Contents - 21.3.10. Algebra

1. Monoids
   1. mndcld
   2. mndassd
   3. mndlrinv
   4. mndlrinvb
   5. mndlactf1
   6. mndlactfo
   7. mndractf1
   8. mndractfo
   9. mndlactf1o
   10. mndractf1o
   11. cmn4d
   12. cmn246135
   13. cmn145236
   14. submcld
2. Monoids Homomorphisms
   1. abliso
   2. lmhmghmd
   3. mhmimasplusg
   4. lmhmimasvsca
3. Groups - misc additions
   1. grpsubcld
   2. subgcld
   3. subgsubcld
   4. subgmulgcld
   5. ressmulgnn0d
4. Finitely supported group sums - misc additions
   1. gsumsubg
   2. gsumsra
   3. gsummpt2co
   4. gsummpt2d
   5. lmodvslmhm
   6. gsumvsmul1
   7. gsummptres
   8. gsummptres2
   9. gsummptfsf1o
   10. gsumfs2d
   11. gsumzresunsn
   12. gsumpart
   13. gsumtp
   14. gsumzrsum
   15. gsummulgc2
   16. gsumhashmul
   17. xrge0tsmsd
   18. xrge0tsmsbi
   19. xrge0tsmseq
5. Group or monoid sums over words
   1. gsumwun
   2. gsumwrd2dccatlem
   3. gsumwrd2dccat
6. Centralizers and centers - misc additions
   1. cntzun
   2. cntzsnid
   3. cntrcrng
7. 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
8. The symmetric group
   1. symgfcoeu
   2. symgcom
   3. symgcom2
   4. symgcntz
   5. odpmco
   6. symgsubg
   7. pmtrprfv2
   8. pmtrcnel
   9. pmtrcnel2
   10. pmtrcnelor
   11. fzo0pmtrlast
   12. wrdpmtrlast
9. Transpositions
   1. pmtridf1o
   2. pmtridfv1
   3. pmtridfv2
10. Permutation Signs
    1. psgnid
    2. psgndmfi
    3. pmtrto1cl
    4. psgnfzto1stlem
    5. fzto1stfv1
    6. fzto1st1
    7. fzto1st
    8. fzto1stinvn
    9. psgnfzto1st
11. 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
12. 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
13. Signum in an ordered monoid
    1. csgns
    2. df-sgns
    3. sgnsv
    4. sgnsval
    5. sgnsf
14. Fixed points
    1. cfxp
    2. df-fxp
    3. fxpval
    4. fxpss
    5. fxpgaval
    6. isfxp
    7. fxpgaeq
    8. conjga
    9. cntrval2
    10. fxpsubm
15. 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
16. 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
17. Simple groups
    1. prmsimpcyc
18. Rings - misc additions
    1. ringdi22
    2. urpropd
    3. subrgmcld
    4. ress1r
    5. ringinvval
    6. dvrcan5
    7. subrgchr
    8. rmfsupp2
    9. unitnz
    10. isunit2
    11. isunit3
19. Subrings generated by a set
    1. elrgspnlem1
    2. elrgspnlem2
    3. elrgspnlem3
    4. elrgspnlem4
    5. elrgspn
    6. elrgspnsubrunlem1
    7. elrgspnsubrunlem2
    8. elrgspnsubrun
20. The zero ring
    1. irrednzr
    2. 0ringsubrg
    3. 0ringcring
21. 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
22. Integral Domains
    1. domnmuln0rd
    2. domnprodn0
    3. domnpropd
    4. idompropd
    5. idomrcan
    6. domnlcanOLD
    7. domnlcanbOLD
    8. idomrcanOLD
    9. 1rrg
    10. rrgsubm
    11. subrdom
    12. subridom
    13. subrfld
23. Euclidean Domains
    1. ceuf
    2. df-euf
    3. eufndx
    4. eufid
    5. cedom
    6. df-edom
24. Division Rings
    1. ringinveu
    2. isdrng4
    3. rndrhmcl
25. The field of rational numbers
    1. qfld
26. Subfields
    1. subsdrg
    2. sdrgdvcl
    3. sdrginvcl
    4. primefldchr
27. Field of fractions
    1. cfrac
    2. df-frac
    3. fracval
    4. fracbas
    5. fracerl
    6. fracf1
    7. fracfld
    8. idomsubr
28. 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
29. 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
30. Ring homomorphisms - misc additions
    1. rhmdvd
    2. kerunit
31. Scalar restriction operation
    1. cresv
    2. df-resv
    3. reldmresv
    4. resvval
    5. resvid2
    6. resvval2
    7. resvsca
    8. resvlem
    9. resvbas
    10. resvplusg
    11. resvvsca
    12. resvmulr
    13. resv0g
    14. resv1r
    15. resvcmn
32. The commutative ring of gaussian integers
    1. gzcrng
33. The archimedean ordered field of real numbers
    1. cnfldfld
    2. reofld
    3. nn0omnd
    4. rearchi
    5. nn0archi
    6. xrge0slmod
34. 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
35. The ring of integers modulo ` N `
    1. znfermltl
36. Independent sets and families
    1. islinds5
    2. ellspds
    3. 0ellsp
    4. 0nellinds
    5. rspsnid
    6. elrsp
    7. ellpi
    8. lpirlidllpi
    9. rspidlid
    10. pidlnz
    11. lbslsp
    12. lindssn
    13. lindflbs
    14. islbs5
    15. linds2eq
    16. lindfpropd
    17. lindspropd
37. Ring associates, ring units
    1. dvdsruassoi
    2. dvdsruasso
    3. dvdsruasso2
    4. dvdsrspss
    5. rspsnasso
    6. unitprodclb
38. 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
39. The quotient map
    1. quslsm
    2. qusbas2
    3. qus0g
    4. qusima
    5. qusrn
    6. nsgqus0
    7. nsgmgclem
    8. nsgmgc
    9. nsgqusf1olem1
    10. nsgqusf1olem2
    11. nsgqusf1olem3
    12. nsgqusf1o
    13. lmhmqusker
    14. lmicqusker
40. Ideals
    1. lidlmcld
    2. intlidl
    3. 0ringidl
    4. pidlnzb
    5. lidlunitel
    6. unitpidl1
    7. rhmquskerlem
    8. rhmqusker
    9. ricqusker
    10. elrspunidl
    11. elrspunsn
    12. lidlincl
    13. idlinsubrg
    14. rhmimaidl
    15. drngidl
    16. drngidlhash
41. 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
    22. ssdifidllem
    23. ssdifidl
    24. ssdifidlprm
42. 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. drngmxidlr
    21. krull
    22. mxidlnzrb
    23. krullndrng
    24. opprabs
    25. oppreqg
    26. opprnsg
    27. opprlidlabs
    28. oppr2idl
    29. opprmxidlabs
    30. opprqusbas
    31. opprqusplusg
    32. opprqus0g
    33. opprqusmulr
    34. opprqus1r
    35. opprqusdrng
    36. qsdrngilem
    37. qsdrngi
    38. qsdrnglem2
    39. qsdrng
    40. qsfld
    41. mxidlprmALT
43. 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
44. 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. rprmasso3
    13. unitmulrprm
    14. rprmndvdsru
    15. rprmirredlem
    16. rprmirred
    17. rprmirredb
    18. rprmdvdspow
    19. rprmdvdsprod
    20. 1arithidomlem1
    21. 1arithidomlem2
    22. 1arithidom
45. Unique factorization domains
    1. cufd
    2. df-ufd
    3. isufd
    4. ufdprmidl
    5. ufdidom
    6. pidufd
    7. 1arithufdlem1
    8. 1arithufdlem2
    9. 1arithufdlem3
    10. 1arithufdlem4
    11. 1arithufd
    12. dfufd2lem
    13. dfufd2
46. The ring of integers
    1. zringidom
    2. zringpid
    3. dfprm3
    4. zringfrac
47. Univariate Polynomials
    1. 0ringmon1p
    2. fply1
    3. ply1lvec
    4. evls1fn
    5. evls1dm
    6. evls1fvf
    7. evl1fvf
    8. evl1fpws
    9. ressply1evls1
    10. ressdeg1
    11. ressply10g
    12. ressply1mon1p
    13. ressply1invg
    14. ressply1sub
    15. ressasclcl
    16. evls1subd
    17. deg1le0eq0
    18. ply1asclunit
    19. ply1unit
    20. evl1deg1
    21. evl1deg2
    22. evl1deg3
    23. ply1dg1rt
    24. ply1dg1rtn0
    25. ply1mulrtss
    26. ply1dg3rt0irred
    27. m1pmeq
    28. ply1fermltl
    29. coe1mon
    30. ply1moneq
    31. coe1zfv
    32. coe1vr1
    33. deg1vr
    34. vr1nz
    35. ply1degltel
    36. ply1degleel
    37. ply1degltlss
    38. gsummoncoe1fzo
    39. ply1gsumz
    40. deg1addlt
    41. ig1pnunit
    42. ig1pmindeg
48. Polynomial quotient and polynomial remainder
    1. q1pdir
    2. q1pvsca
    3. r1pvsca
    4. r1p0
    5. r1pcyc
    6. r1padd1
    7. r1pid2OLD
    8. r1plmhm
    9. r1pquslmic
49. The subring algebra
    1. sra1r
    2. sradrng
    3. sraidom
    4. srasubrg
    5. sralvec
    6. srafldlvec
    7. resssra
    8. lsssra
50. Division Ring Extensions
    1. drgext0g
    2. drgextvsca
    3. drgext0gsca
    4. drgextsubrg
    5. drgextlsp
    6. drgextgsum
51. Vector Spaces
    1. lvecdimfi
    2. exsslsb
    3. lbslelsp
52. 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
    35. dimlssid
    36. lvecendof1f1o
    37. lactlmhm
    38. assalactf1o
    39. assarrginv
    40. assafld