![]() |
Metamath
Proof Explorer Theorem List (p. 202 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ringcmnd 20101 | A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
โข (๐ โ ๐ โ Ring) โ โข (๐ โ ๐ โ CMnd) | ||
Theorem | ringpropd 20102* | If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a ring iff the other one is. (Contributed by Mario Carneiro, 6-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
โข (๐ โ ๐ต = (Baseโ๐พ)) & โข (๐ โ ๐ต = (Baseโ๐ฟ)) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐พ)๐ฆ) = (๐ฅ(+gโ๐ฟ)๐ฆ)) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(.rโ๐พ)๐ฆ) = (๐ฅ(.rโ๐ฟ)๐ฆ)) โ โข (๐ โ (๐พ โ Ring โ ๐ฟ โ Ring)) | ||
Theorem | crngpropd 20103* | If two structures have the same group components (properties), one is a commutative ring iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
โข (๐ โ ๐ต = (Baseโ๐พ)) & โข (๐ โ ๐ต = (Baseโ๐ฟ)) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐พ)๐ฆ) = (๐ฅ(+gโ๐ฟ)๐ฆ)) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(.rโ๐พ)๐ฆ) = (๐ฅ(.rโ๐ฟ)๐ฆ)) โ โข (๐ โ (๐พ โ CRing โ ๐ฟ โ CRing)) | ||
Theorem | ringprop 20104 | If two structures have the same ring components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) |
โข (Baseโ๐พ) = (Baseโ๐ฟ) & โข (+gโ๐พ) = (+gโ๐ฟ) & โข (.rโ๐พ) = (.rโ๐ฟ) โ โข (๐พ โ Ring โ ๐ฟ โ Ring) | ||
Theorem | isringd 20105* | Properties that determine a ring. (Contributed by NM, 2-Aug-2013.) |
โข (๐ โ ๐ต = (Baseโ๐ )) & โข (๐ โ + = (+gโ๐ )) & โข (๐ โ ยท = (.rโ๐ )) & โข (๐ โ ๐ โ Grp) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ ยท ๐ฆ) โ ๐ต) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง))) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) & โข (๐ โ 1 โ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ต) โ ( 1 ยท ๐ฅ) = ๐ฅ) & โข ((๐ โง ๐ฅ โ ๐ต) โ (๐ฅ ยท 1 ) = ๐ฅ) โ โข (๐ โ ๐ โ Ring) | ||
Theorem | iscrngd 20106* | Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
โข (๐ โ ๐ต = (Baseโ๐ )) & โข (๐ โ + = (+gโ๐ )) & โข (๐ โ ยท = (.rโ๐ )) & โข (๐ โ ๐ โ Grp) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ ยท ๐ฆ) โ ๐ต) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง))) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง))) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))) & โข (๐ โ 1 โ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ต) โ ( 1 ยท ๐ฅ) = ๐ฅ) & โข ((๐ โง ๐ฅ โ ๐ต) โ (๐ฅ ยท 1 ) = ๐ฅ) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ)) โ โข (๐ โ ๐ โ CRing) | ||
Theorem | ringlz 20107 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต) โ ( 0 ยท ๐) = 0 ) | ||
Theorem | ringrz 20108 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) | ||
Theorem | ringsrg 20109 | Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
โข (๐ โ Ring โ ๐ โ SRing) | ||
Theorem | ring1eq0 20110 | If one and zero are equal, then any two elements of a ring are equal. Alternately, every ring has one distinct from zero except the zero ring containing the single element {0}. (Contributed by Mario Carneiro, 10-Sep-2014.) |
โข ๐ต = (Baseโ๐ ) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ( 1 = 0 โ ๐ = ๐)) | ||
Theorem | ring1ne0 20111 | If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019.) |
โข ๐ต = (Baseโ๐ ) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Ring โง 1 < (โฏโ๐ต)) โ 1 โ 0 ) | ||
Theorem | ringinvnz1ne0 20112* | In a unital ring, a left invertible element is different from zero iff 1 โ 0. (Contributed by FL, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ โ๐ โ ๐ต (๐ ยท ๐) = 1 ) โ โข (๐ โ (๐ โ 0 โ 1 โ 0 )) | ||
Theorem | ringinvnzdiv 20113* | In a unital ring, a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010.) (Revised by Jeff Madsen, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 1 = (1rโ๐ ) & โข 0 = (0gโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ โ๐ โ ๐ต (๐ ยท ๐) = 1 ) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ ยท ๐) = 0 โ ๐ = 0 )) | ||
Theorem | ringnegl 20114 | Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 36809 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (invgโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐โ 1 ) ยท ๐) = (๐โ๐)) | ||
Theorem | ringnegr 20115 | Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 36810 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (invgโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ ยท (๐โ 1 )) = (๐โ๐)) | ||
Theorem | ringmneg1 20116 | Negation of a product in a ring. (mulneg1 11650 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (invgโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐โ๐) ยท ๐) = (๐โ(๐ ยท ๐))) | ||
Theorem | ringmneg2 20117 | Negation of a product in a ring. (mulneg2 11651 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (invgโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ ยท (๐โ๐)) = (๐โ(๐ ยท ๐))) | ||
Theorem | ringm2neg 20118 | Double negation of a product in a ring. (mul2neg 11653 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (invgโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐โ๐) ยท (๐โ๐)) = (๐ ยท ๐)) | ||
Theorem | ringsubdi 20119 | Ring multiplication distributes over subtraction. (subdi 11647 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข โ = (-gโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ ยท (๐ โ ๐)) = ((๐ ยท ๐) โ (๐ ยท ๐))) | ||
Theorem | ringsubdir 20120 | Ring multiplication distributes over subtraction. (subdir 11648 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข โ = (-gโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ ๐) ยท ๐) = ((๐ ยท ๐) โ (๐ ยท ๐))) | ||
Theorem | mulgass2 20121 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.gโ๐ ) & โข ร = (.rโ๐ ) โ โข ((๐ โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ร ๐) = (๐ ยท (๐ ร ๐))) | ||
Theorem | ring1 20122 | The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.) |
โข ๐ = {โจ(Baseโndx), {๐}โฉ, โจ(+gโndx), {โจโจ๐, ๐โฉ, ๐โฉ}โฉ, โจ(.rโndx), {โจโจ๐, ๐โฉ, ๐โฉ}โฉ} โ โข (๐ โ ๐ โ ๐ โ Ring) | ||
Theorem | ringn0 20123 | Rings exist. (Contributed by AV, 29-Apr-2019.) |
โข Ring โ โ | ||
Theorem | ringlghm 20124* | Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต) โ (๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ)) โ (๐ GrpHom ๐ )) | ||
Theorem | ringrghm 20125* | Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต) โ (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)) โ (๐ GrpHom ๐ )) | ||
Theorem | gsummulc1OLD 20126* | Obsolete version of gsummulc1 20128 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ต = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ โ ๐ด) โ ๐ โ ๐ต) & โข (๐ โ (๐ โ ๐ด โฆ ๐) finSupp 0 ) โ โข (๐ โ (๐ ฮฃg (๐ โ ๐ด โฆ (๐ ยท ๐))) = ((๐ ฮฃg (๐ โ ๐ด โฆ ๐)) ยท ๐)) | ||
Theorem | gsummulc2OLD 20127* | Obsolete version of gsummulc2 20129 as of 7-Mar-2025. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ต = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ โ ๐ด) โ ๐ โ ๐ต) & โข (๐ โ (๐ โ ๐ด โฆ ๐) finSupp 0 ) โ โข (๐ โ (๐ ฮฃg (๐ โ ๐ด โฆ (๐ ยท ๐))) = (๐ ยท (๐ ฮฃg (๐ โ ๐ด โฆ ๐)))) | ||
Theorem | gsummulc1 20128* | A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) Remove unused hypothesis. (Revised by SN, 7-Mar-2025.) |
โข ๐ต = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ โ ๐ด) โ ๐ โ ๐ต) & โข (๐ โ (๐ โ ๐ด โฆ ๐) finSupp 0 ) โ โข (๐ โ (๐ ฮฃg (๐ โ ๐ด โฆ (๐ ยท ๐))) = ((๐ ฮฃg (๐ โ ๐ด โฆ ๐)) ยท ๐)) | ||
Theorem | gsummulc2 20129* | A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) Remove unused hypothesis. (Revised by SN, 7-Mar-2025.) |
โข ๐ต = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ โ ๐ด) โ ๐ โ ๐ต) & โข (๐ โ (๐ โ ๐ด โฆ ๐) finSupp 0 ) โ โข (๐ โ (๐ ฮฃg (๐ โ ๐ด โฆ (๐ ยท ๐))) = (๐ ยท (๐ ฮฃg (๐ โ ๐ด โฆ ๐)))) | ||
Theorem | gsummgp0 20130* | If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019.) |
โข ๐บ = (mulGrpโ๐ ) & โข 0 = (0gโ๐ ) & โข (๐ โ ๐ โ CRing) & โข (๐ โ ๐ โ Fin) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ (Baseโ๐ )) & โข ((๐ โง ๐ = ๐) โ ๐ด = ๐ต) & โข (๐ โ โ๐ โ ๐ ๐ต = 0 ) โ โข (๐ โ (๐บ ฮฃg (๐ โ ๐ โฆ ๐ด)) = 0 ) | ||
Theorem | gsumdixp 20131* | Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.) (Revised by AV, 10-Jul-2019.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 0 = (0gโ๐ ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ฝ โ ๐) & โข (๐ โ ๐ โ Ring) & โข ((๐ โง ๐ฅ โ ๐ผ) โ ๐ โ ๐ต) & โข ((๐ โง ๐ฆ โ ๐ฝ) โ ๐ โ ๐ต) & โข (๐ โ (๐ฅ โ ๐ผ โฆ ๐) finSupp 0 ) & โข (๐ โ (๐ฆ โ ๐ฝ โฆ ๐) finSupp 0 ) โ โข (๐ โ ((๐ ฮฃg (๐ฅ โ ๐ผ โฆ ๐)) ยท (๐ ฮฃg (๐ฆ โ ๐ฝ โฆ ๐))) = (๐ ฮฃg (๐ฅ โ ๐ผ, ๐ฆ โ ๐ฝ โฆ (๐ ยท ๐)))) | ||
Theorem | prdsmgp 20132 | The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐Xs๐ ) & โข ๐ = (mulGrpโ๐) & โข ๐ = (๐Xs(mulGrp โ ๐ )) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ Fn ๐ผ) โ โข (๐ โ ((Baseโ๐) = (Baseโ๐) โง (+gโ๐) = (+gโ๐))) | ||
Theorem | prdsmulrcl 20133 | A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐Xs๐ ) & โข ๐ต = (Baseโ๐) & โข ยท = (.rโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ :๐ผโถRing) & โข (๐ โ ๐น โ ๐ต) & โข (๐ โ ๐บ โ ๐ต) โ โข (๐ โ (๐น ยท ๐บ) โ ๐ต) | ||
Theorem | prdsringd 20134 | A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐Xs๐ ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ :๐ผโถRing) โ โข (๐ โ ๐ โ Ring) | ||
Theorem | prdscrngd 20135 | A product of commutative rings is a commutative ring. Since the resulting ring will have zero divisors in all nontrivial cases, this cannot be strengthened much further. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐Xs๐ ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ :๐ผโถCRing) โ โข (๐ โ ๐ โ CRing) | ||
Theorem | prds1 20136 | Value of the ring unity in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐Xs๐ ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ :๐ผโถRing) โ โข (๐ โ (1r โ ๐ ) = (1rโ๐)) | ||
Theorem | pwsring 20137 | A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐ โs ๐ผ) โ โข ((๐ โ Ring โง ๐ผ โ ๐) โ ๐ โ Ring) | ||
Theorem | pws1 20138 | Value of the ring unity in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐ โs ๐ผ) & โข 1 = (1rโ๐ ) โ โข ((๐ โ Ring โง ๐ผ โ ๐) โ (๐ผ ร { 1 }) = (1rโ๐)) | ||
Theorem | pwscrng 20139 | A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐ โs ๐ผ) โ โข ((๐ โ CRing โง ๐ผ โ ๐) โ ๐ โ CRing) | ||
Theorem | pwsmgp 20140 | The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015.) |
โข ๐ = (๐ โs ๐ผ) & โข ๐ = (mulGrpโ๐ ) & โข ๐ = (๐ โs ๐ผ) & โข ๐ = (mulGrpโ๐) & โข ๐ต = (Baseโ๐) & โข ๐ถ = (Baseโ๐) & โข + = (+gโ๐) & โข โ = (+gโ๐) โ โข ((๐ โ ๐ โง ๐ผ โ ๐) โ (๐ต = ๐ถ โง + = โ )) | ||
Theorem | pwspjmhmmgpd 20141* | The projection given by pwspjmhm 18711 is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024.) |
โข ๐ = (๐ โs ๐ผ) & โข ๐ต = (Baseโ๐) & โข ๐ = (mulGrpโ๐) & โข ๐ = (mulGrpโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ด โ ๐ผ) โ โข (๐ โ (๐ฅ โ ๐ต โฆ (๐ฅโ๐ด)) โ (๐ MndHom ๐)) | ||
Theorem | pwsexpg 20142 | Value of a group exponentiation in a structure power. Compare pwsmulg 18999. (Contributed by SN, 30-Jul-2024.) |
โข ๐ = (๐ โs ๐ผ) & โข ๐ต = (Baseโ๐) & โข ๐ = (mulGrpโ๐) & โข ๐ = (mulGrpโ๐ ) & โข โ = (.gโ๐) & โข ยท = (.gโ๐) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ด โ ๐ผ) โ โข (๐ โ ((๐ โ ๐)โ๐ด) = (๐ ยท (๐โ๐ด))) | ||
Theorem | imasring 20143* | The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข (๐ โ ๐ = (๐น โs ๐ )) & โข (๐ โ ๐ = (Baseโ๐ )) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข 1 = (1rโ๐ ) & โข (๐ โ ๐น:๐โontoโ๐ต) & โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐)) โ (๐นโ(๐ + ๐)) = (๐นโ(๐ + ๐)))) & โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐)) โ (๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐)))) & โข (๐ โ ๐ โ Ring) โ โข (๐ โ (๐ โ Ring โง (๐นโ 1 ) = (1rโ๐))) | ||
Theorem | imasringf1 20144 | The image of a ring under an injection is a ring (imasmndf1 18664 analog). (Contributed by AV, 27-Feb-2025.) |
โข ๐ = (๐น โs ๐ ) & โข ๐ = (Baseโ๐ ) โ โข ((๐น:๐โ1-1โ๐ต โง ๐ โ Ring) โ ๐ โ Ring) | ||
Theorem | xpsringd 20145 | A product of two rings is a ring (xpsmnd 18665 analog). (Contributed by AV, 28-Feb-2025.) |
โข ๐ = (๐ รs ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ Ring) โ โข (๐ โ ๐ โ Ring) | ||
Theorem | xpsring1d 20146 | The multiplicative identity element of a binary product of rings. (Contributed by AV, 16-Mar-2025.) |
โข ๐ = (๐ รs ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ Ring) โ โข (๐ โ (1rโ๐) = โจ(1rโ๐), (1rโ๐ )โฉ) | ||
Theorem | qusring2 20147* | The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข (๐ โ ๐ = (๐ /s โผ )) & โข (๐ โ ๐ = (Baseโ๐ )) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข 1 = (1rโ๐ ) & โข (๐ โ โผ Er ๐) & โข (๐ โ ((๐ โผ ๐ โง ๐ โผ ๐) โ (๐ + ๐) โผ (๐ + ๐))) & โข (๐ โ ((๐ โผ ๐ โง ๐ โผ ๐) โ (๐ ยท ๐) โผ (๐ ยท ๐))) & โข (๐ โ ๐ โ Ring) โ โข (๐ โ (๐ โ Ring โง [ 1 ] โผ = (1rโ๐))) | ||
Theorem | crngbinom 20148* | The binomial theorem for commutative rings (special case of csrgbinom 20055): (๐ด + ๐ต)โ๐ is the sum from ๐ = 0 to ๐ of (๐C๐) ยท ((๐ดโ๐) ยท (๐ตโ(๐ โ ๐)). (Contributed by AV, 24-Aug-2019.) |
โข ๐ = (Baseโ๐ ) & โข ร = (.rโ๐ ) & โข ยท = (.gโ๐ ) & โข + = (+gโ๐ ) & โข ๐บ = (mulGrpโ๐ ) & โข โ = (.gโ๐บ) โ โข (((๐ โ CRing โง ๐ โ โ0) โง (๐ด โ ๐ โง ๐ต โ ๐)) โ (๐ โ (๐ด + ๐ต)) = (๐ ฮฃg (๐ โ (0...๐) โฆ ((๐C๐) ยท (((๐ โ ๐) โ ๐ด) ร (๐ โ ๐ต)))))) | ||
Syntax | coppr 20149 | The opposite ring operation. |
class oppr | ||
Definition | df-oppr 20150 | Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข oppr = (๐ โ V โฆ (๐ sSet โจ(.rโndx), tpos (.rโ๐)โฉ)) | ||
Theorem | opprval 20151 | Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (opprโ๐ ) โ โข ๐ = (๐ sSet โจ(.rโndx), tpos ยท โฉ) | ||
Theorem | opprmulfval 20152 | Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (opprโ๐ ) & โข โ = (.rโ๐) โ โข โ = tpos ยท | ||
Theorem | opprmul 20153 | Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (opprโ๐ ) & โข โ = (.rโ๐) โ โข (๐ โ ๐) = (๐ ยท ๐) | ||
Theorem | crngoppr 20154 | In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 20231). (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (opprโ๐ ) & โข โ = (.rโ๐) โ โข ((๐ โ CRing โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) = (๐ โ ๐)) | ||
Theorem | opprlem 20155 | Lemma for opprbas 20157 and oppradd 20159. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) |
โข ๐ = (opprโ๐ ) & โข ๐ธ = Slot (๐ธโndx) & โข (๐ธโndx) โ (.rโndx) โ โข (๐ธโ๐ ) = (๐ธโ๐) | ||
Theorem | opprlemOLD 20156 | Obsolete version of opprlem 20155 as of 6-Nov-2024. Lemma for opprbas 20157 and oppradd 20159. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ๐ = (opprโ๐ ) & โข ๐ธ = Slot ๐ & โข ๐ โ โ & โข ๐ < 3 โ โข (๐ธโ๐ ) = (๐ธโ๐) | ||
Theorem | opprbas 20157 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
โข ๐ = (opprโ๐ ) & โข ๐ต = (Baseโ๐ ) โ โข ๐ต = (Baseโ๐) | ||
Theorem | opprbasOLD 20158 | Obsolete proof of opprbas 20157 as of 6-Nov-2024. Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ๐ = (opprโ๐ ) & โข ๐ต = (Baseโ๐ ) โ โข ๐ต = (Baseโ๐) | ||
Theorem | oppradd 20159 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
โข ๐ = (opprโ๐ ) & โข + = (+gโ๐ ) โ โข + = (+gโ๐) | ||
Theorem | oppraddOLD 20160 | Obsolete proof of opprbas 20157 as of 6-Nov-2024. Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ๐ = (opprโ๐ ) & โข + = (+gโ๐ ) โ โข + = (+gโ๐) | ||
Theorem | opprring 20161 | An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) |
โข ๐ = (opprโ๐ ) โ โข (๐ โ Ring โ ๐ โ Ring) | ||
Theorem | opprringb 20162 | Bidirectional form of opprring 20161. (Contributed by Mario Carneiro, 6-Dec-2014.) |
โข ๐ = (opprโ๐ ) โ โข (๐ โ Ring โ ๐ โ Ring) | ||
Theorem | oppr0 20163 | Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ = (opprโ๐ ) & โข 0 = (0gโ๐ ) โ โข 0 = (0gโ๐) | ||
Theorem | oppr1 20164 | Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ = (opprโ๐ ) & โข 1 = (1rโ๐ ) โ โข 1 = (1rโ๐) | ||
Theorem | opprneg 20165 | The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
โข ๐ = (opprโ๐ ) & โข ๐ = (invgโ๐ ) โ โข ๐ = (invgโ๐) | ||
Theorem | opprsubg 20166 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
โข ๐ = (opprโ๐ ) โ โข (SubGrpโ๐ ) = (SubGrpโ๐) | ||
Theorem | mulgass3 20167 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.gโ๐ ) & โข ร = (.rโ๐ ) โ โข ((๐ โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ร (๐ ยท ๐)) = (๐ ยท (๐ ร ๐))) | ||
Syntax | cdsr 20168 | Ring divisibility relation. |
class โฅr | ||
Syntax | cui 20169 | Units in a ring. |
class Unit | ||
Syntax | cir 20170 | Ring irreducibles. |
class Irred | ||
Definition | df-dvdsr 20171* | Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through (โฅrโ(opprโ๐ )). (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข โฅr = (๐ค โ V โฆ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐ค) โง โ๐ง โ (Baseโ๐ค)(๐ง(.rโ๐ค)๐ฅ) = ๐ฆ)}) | ||
Definition | df-unit 20172 | Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข Unit = (๐ค โ V โฆ (โก((โฅrโ๐ค) โฉ (โฅrโ(opprโ๐ค))) โ {(1rโ๐ค)})) | ||
Definition | df-irred 20173* | Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
โข Irred = (๐ค โ V โฆ โฆ((Baseโ๐ค) โ (Unitโ๐ค)) / ๐โฆ{๐ง โ ๐ โฃ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ(.rโ๐ค)๐ฆ) โ ๐ง}) | ||
Theorem | reldvdsr 20174 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข โฅ = (โฅrโ๐ ) โ โข Rel โฅ | ||
Theorem | dvdsrval 20175* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข ยท = (.rโ๐ ) โ โข โฅ = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} | ||
Theorem | dvdsr 20176* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข ยท = (.rโ๐ ) โ โข (๐ โฅ ๐ โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐)) | ||
Theorem | dvdsr2 20177* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข ยท = (.rโ๐ ) โ โข (๐ โ ๐ต โ (๐ โฅ ๐ โ โ๐ง โ ๐ต (๐ง ยท ๐) = ๐)) | ||
Theorem | dvdsrmul 20178 | A left-multiple of ๐ is divisible by ๐. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โฅ (๐ ยท ๐)) | ||
Theorem | dvdsrcl 20179 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) โ โข (๐ โฅ ๐ โ ๐ โ ๐ต) | ||
Theorem | dvdsrcl2 20180 | Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) โ โข ((๐ โ Ring โง ๐ โฅ ๐) โ ๐ โ ๐ต) | ||
Theorem | dvdsrid 20181 | An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต) โ ๐ โฅ ๐) | ||
Theorem | dvdsrtr 20182 | Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) โ โข ((๐ โ Ring โง ๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ โฅ ๐) | ||
Theorem | dvdsrmul1 20183 | The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต โง ๐ โฅ ๐) โ (๐ ยท ๐) โฅ (๐ ยท ๐)) | ||
Theorem | dvdsrneg 20184 | An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข ๐ = (invgโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต) โ ๐ โฅ (๐โ๐)) | ||
Theorem | dvdsr01 20185 | In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 20899.) (Contributed by Stefan O'Rear, 29-Mar-2015.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต) โ ๐ โฅ 0 ) | ||
Theorem | dvdsr02 20186 | Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
โข ๐ต = (Baseโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ต) โ ( 0 โฅ ๐ โ ๐ = 0 )) | ||
Theorem | isunit 20187 | Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.) |
โข ๐ = (Unitโ๐ ) & โข 1 = (1rโ๐ ) & โข โฅ = (โฅrโ๐ ) & โข ๐ = (opprโ๐ ) & โข ๐ธ = (โฅrโ๐) โ โข (๐ โ ๐ โ (๐ โฅ 1 โง ๐๐ธ 1 )) | ||
Theorem | 1unit 20188 | The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ = (Unitโ๐ ) & โข 1 = (1rโ๐ ) โ โข (๐ โ Ring โ 1 โ ๐) | ||
Theorem | unitcl 20189 | A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.) |
โข ๐ต = (Baseโ๐ ) & โข ๐ = (Unitโ๐ ) โ โข (๐ โ ๐ โ ๐ โ ๐ต) | ||
Theorem | unitss 20190 | The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ๐ = (Unitโ๐ ) โ โข ๐ โ ๐ต | ||
Theorem | opprunit 20191 | Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
โข ๐ = (Unitโ๐ ) & โข ๐ = (opprโ๐ ) โ โข ๐ = (Unitโ๐) | ||
Theorem | crngunit 20192 | Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
โข ๐ = (Unitโ๐ ) & โข 1 = (1rโ๐ ) & โข โฅ = (โฅrโ๐ ) โ โข (๐ โ CRing โ (๐ โ ๐ โ ๐ โฅ 1 )) | ||
Theorem | dvdsunit 20193 | A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.) |
โข ๐ = (Unitโ๐ ) & โข โฅ = (โฅrโ๐ ) โ โข ((๐ โ CRing โง ๐ โฅ ๐ โง ๐ โ ๐) โ ๐ โ ๐) | ||
Theorem | unitmulcl 20194 | The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ = (Unitโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | unitmulclb 20195 | Reversal of unitmulcl 20194 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.) |
โข ๐ = (Unitโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ต = (Baseโ๐ ) โ โข ((๐ โ CRing โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ ยท ๐) โ ๐ โ (๐ โ ๐ โง ๐ โ ๐))) | ||
Theorem | unitgrpbas 20196 | The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.) |
โข ๐ = (Unitโ๐ ) & โข ๐บ = ((mulGrpโ๐ ) โพs ๐) โ โข ๐ = (Baseโ๐บ) | ||
Theorem | unitgrp 20197 | The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ = (Unitโ๐ ) & โข ๐บ = ((mulGrpโ๐ ) โพs ๐) โ โข (๐ โ Ring โ ๐บ โ Grp) | ||
Theorem | unitabl 20198 | The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.) |
โข ๐ = (Unitโ๐ ) & โข ๐บ = ((mulGrpโ๐ ) โพs ๐) โ โข (๐ โ CRing โ ๐บ โ Abel) | ||
Theorem | unitgrpid 20199 | The identity of the group of units of a ring is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ = (Unitโ๐ ) & โข ๐บ = ((mulGrpโ๐ ) โพs ๐) & โข 1 = (1rโ๐ ) โ โข (๐ โ Ring โ 1 = (0gโ๐บ)) | ||
Theorem | unitsubm 20200 | The group of units is a submonoid of the multiplicative monoid of the ring. (Contributed by Mario Carneiro, 18-Jun-2015.) |
โข ๐ = (Unitโ๐ ) & โข ๐ = (mulGrpโ๐ ) โ โข (๐ โ Ring โ ๐ โ (SubMndโ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |