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. gsumzresunsn
    9. xrge0tsmsd
    10. xrge0tsmsbi
    11. 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. ress1r
    5. dvrdir
    6. rdivmuldivd
    7. ringinvval
    8. dvrcan5
    9. subrgchr
    10. 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. resvbas
    10. resvplusg
    11. resvvsca
    12. resvmulr
    13. resv0g
    14. resv1r
    15. 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. Univariate Polynomials
    1. fply1
  23. Independent sets and families
    1. islinds5
    2. ellspds
    3. 0ellsp
    4. 0nellinds
    5. rspsnel
    6. rspsnid
    7. pidlnz
    8. lbslsp
    9. lindssn
    10. lindflbs
    11. linds2eq
    12. lindfpropd
    13. lindspropd
  24. Subgroup sum / Sumset / Minkowski sum
    1. elgrplsmsn
    2. lsmsnorb
    3. elringlsm
    4. elringlsmd
    5. ringlsmss
    6. lsmsnpridl
    7. lsmsnidl
    8. lsmidllsp
    9. lsmidl
  25. Prime Ideals
    1. cprmidl
    2. df-prmidl
    3. prmidlval
    4. isprmidl
    5. prmidlnr
    6. prmidl
    7. prmidl2
    8. idlmulssprm
    9. pridln1
    10. prmidlidl
    11. lidlnsg
    12. cringm4
    13. isprmidlc
    14. prmidlc
    15. qsidomlem1
    16. qsidomlem2
    17. qsidom
  26. 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
  27. The semiring of ideals of a ring
    1. cidlsrg
    2. df-idlsrg
    3. crspec
    4. df-rspec
  28. The subring algebra
    1. sra1r
    2. sraring
    3. sradrng
    4. srasubrg
    5. sralvec
    6. srafldlvec
  29. Division Ring Extensions
    1. drgext0g
    2. drgextvsca
    3. drgext0gsca
    4. drgextsubrg
    5. drgextlsp
    6. drgextgsum
  30. Vector Spaces
    1. lvecdimfi
  31. 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