![]() |
Metamath
Proof Explorer Theorem List (p. 202 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | srgcom 20101 | Commutativity of the additive group of a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β SRing β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) | ||
Theorem | srgrz 20102 | The zero of a semiring is a right-absorbing element. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β SRing β§ π β π΅) β (π Β· 0 ) = 0 ) | ||
Theorem | srglz 20103 | The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β SRing β§ π β π΅) β ( 0 Β· π) = 0 ) | ||
Theorem | srgisid 20104* | In a semiring, the only left-absorbing element is the additive identity. Remark in [Golan] p. 1. (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β SRing) & β’ (π β π β π΅) & β’ ((π β§ π₯ β π΅) β (π Β· π₯) = π) β β’ (π β π = 0 ) | ||
Theorem | o2timesd 20105* | An element of a ring-like structure plus itself is two times the element. "Two" in such a structure is the sum of the unity element with itself. This (formerly) part of the proof for ringcom 20169 depends on the (right) distributivity and the existence of a (left) multiplicative identity only. (Contributed by GΓ©rard Lang, 4-Dec-2014.) (Revised by AV, 1-Feb-2025.) |
β’ (π β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ (π β 1 β π΅) & β’ (π β βπ₯ β π΅ ( 1 Β· π₯) = π₯) & β’ (π β π β π΅) β β’ (π β (π + π) = (( 1 + 1 ) Β· π)) | ||
Theorem | rglcom4d 20106* | Restricted commutativity of the addition in a ring-like structure. This (formerly) part of the proof for ringcom 20169 depends on the closure of the addition, the (left and right) distributivity and the existence of a (left) multiplicative identity only. (Contributed by GΓ©rard Lang, 4-Dec-2014.) (Revised by AV, 1-Feb-2025.) |
β’ (π β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ (π β 1 β π΅) & β’ (π β βπ₯ β π΅ ( 1 Β· π₯) = π₯) & β’ (π β π β π΅) & β’ (π β βπ₯ β π΅ βπ¦ β π΅ (π₯ + π¦) β π΅) & β’ (π β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) & β’ (π β π β π΅) β β’ (π β ((π + π) + (π + π)) = ((π + π) + (π + π))) | ||
Theorem | srgo2times 20107 | A semiring element plus itself is two times the element. "Two" in an arbitrary (unital) semiring is the sum of the unity element with itself. (Contributed by AV, 24-Aug-2021.) Variant of o2timesd 20105 for semirings. (Revised by AV, 1-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β SRing β§ π΄ β π΅) β (π΄ + π΄) = (( 1 + 1 ) Β· π΄)) | ||
Theorem | srgcom4lem 20108 | Lemma for srgcom4 20109. This (formerly) part of the proof for ringcom 20169 is applicable for semirings (without using the commutativity of the addition given per definition of a semiring). (Contributed by GΓ©rard Lang, 4-Dec-2014.) (Revised by AV, 1-Feb-2025.) (Proof modification is discouraged.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β SRing β§ π β π΅ β§ π β π΅) β ((π + π) + (π + π)) = ((π + π) + (π + π))) | ||
Theorem | srgcom4 20109 | Restricted commutativity of the addition in semirings (without using the commutativity of the addition given per definition of a semiring). (Contributed by AV, 1-Feb-2025.) (Proof modification is discouraged.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β SRing β§ π β π΅ β§ π β π΅) β ((π + (π + π)) + π) = ((π + (π + π)) + π)) | ||
Theorem | srg1zr 20110 | The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ β = (.rβπ ) β β’ (((π β SRing β§ + Fn (π΅ Γ π΅) β§ β Fn (π΅ Γ π΅)) β§ π β π΅) β (π΅ = {π} β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
Theorem | srgen1zr 20111 | The only semiring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ β = (.rβπ ) & β’ π = (0gβπ ) β β’ ((π β SRing β§ + Fn (π΅ Γ π΅) β§ β Fn (π΅ Γ π΅)) β (π΅ β 1o β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
Theorem | srgmulgass 20112 | An associative property between group multiple and ring multiplication for semirings. (Contributed by AV, 23-Aug-2019.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.gβπ ) & β’ Γ = (.rβπ ) β β’ ((π β SRing β§ (π β β0 β§ π β π΅ β§ π β π΅)) β ((π Β· π) Γ π) = (π Β· (π Γ π))) | ||
Theorem | srgpcomp 20113 | If two elements of a semiring commute, they also commute if one of the elements is raised to a higher power. (Contributed by AV, 23-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΎ β β0) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) β β’ (π β ((πΎ β π΅) Γ π΄) = (π΄ Γ (πΎ β π΅))) | ||
Theorem | srgpcompp 20114 | If two elements of a semiring commute, they also commute if the elements are raised to a higher power. (Contributed by AV, 23-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΎ β β0) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) β β’ (π β (((π β π΄) Γ (πΎ β π΅)) Γ π΄) = (((π + 1) β π΄) Γ (πΎ β π΅))) | ||
Theorem | srgpcomppsc 20115 | If two elements of a semiring commute, they also commute if the elements are raised to a higher power and a scalar multiplication is involved. (Contributed by AV, 23-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΎ β β0) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) & β’ Β· = (.gβπ ) & β’ (π β πΆ β β0) β β’ (π β ((πΆ Β· ((π β π΄) Γ (πΎ β π΅))) Γ π΄) = (πΆ Β· (((π + 1) β π΄) Γ (πΎ β π΅)))) | ||
Theorem | srglmhm 20116* | Left-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringlghm 20201. (Contributed by AV, 23-Aug-2019.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ π β π΅) β (π₯ β π΅ β¦ (π Β· π₯)) β (π MndHom π )) | ||
Theorem | srgrmhm 20117* | Right-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringrghm 20202. (Contributed by AV, 23-Aug-2019.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ π β π΅) β (π₯ β π΅ β¦ (π₯ Β· π)) β (π MndHom π )) | ||
Theorem | srgsummulcr 20118* | A finite semiring sum multiplied by a constant, analogous to gsummulc1 20205. (Contributed by AV, 23-Aug-2019.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π β π΅) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = ((π Ξ£g (π β π΄ β¦ π)) Β· π)) | ||
Theorem | sgsummulcl 20119* | A finite semiring sum multiplied by a constant, analogous to gsummulc2 20206. (Contributed by AV, 23-Aug-2019.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π β π΅) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) | ||
Theorem | srg1expzeq1 20120 | The exponentiation (by a nonnegative integer) of the multiplicative identity of a semiring, analogous to mulgnn0z 19018. (Contributed by AV, 25-Nov-2019.) |
β’ πΊ = (mulGrpβπ ) & β’ Β· = (.gβπΊ) & β’ 1 = (1rβπ ) β β’ ((π β SRing β§ π β β0) β (π Β· 1 ) = 1 ) | ||
In this section, we prove the binomial theorem for semirings, srgbinom 20126, which is a generalization of the binomial theorem for complex numbers, binom 15781: (π΄ + π΅)βπ is the sum from π = 0 to π of (πCπ) Β· ((π΄βπ) Β· (π΅β(π β π)). Note that the binomial theorem also holds in the non-unital case (that is, in a "rg") and actually, the additive identity is not needed in its proof either. Therefore, it can be proven in even more general cases. An example is the "rg" (resp. "rg without a zero") of integrable nonnegative (resp. positive) functions on β. Special cases of the binomial theorem are csrgbinom 20127 (binomial theorem for commutative semirings) and crngbinom 20224 (binomial theorem for commutative rings). | ||
Theorem | srgbinomlem1 20121 | Lemma 1 for srgbinomlem 20125. (Contributed by AV, 23-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ Β· = (.gβπ ) & β’ + = (+gβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) β β’ ((π β§ (π· β β0 β§ πΈ β β0)) β ((π· β π΄) Γ (πΈ β π΅)) β π) | ||
Theorem | srgbinomlem2 20122 | Lemma 2 for srgbinomlem 20125. (Contributed by AV, 23-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ Β· = (.gβπ ) & β’ + = (+gβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) β β’ ((π β§ (πΆ β β0 β§ π· β β0 β§ πΈ β β0)) β (πΆ Β· ((π· β π΄) Γ (πΈ β π΅))) β π) | ||
Theorem | srgbinomlem3 20123* | Lemma 3 for srgbinomlem 20125. (Contributed by AV, 23-Aug-2019.) (Proof shortened by AV, 27-Oct-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ Β· = (.gβπ ) & β’ + = (+gβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) & β’ (π β (π β (π΄ + π΅)) = (π Ξ£g (π β (0...π) β¦ ((πCπ) Β· (((π β π) β π΄) Γ (π β π΅)))))) β β’ ((π β§ π) β ((π β (π΄ + π΅)) Γ π΄) = (π Ξ£g (π β (0...(π + 1)) β¦ ((πCπ) Β· ((((π + 1) β π) β π΄) Γ (π β π΅)))))) | ||
Theorem | srgbinomlem4 20124* | Lemma 4 for srgbinomlem 20125. (Contributed by AV, 24-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ Β· = (.gβπ ) & β’ + = (+gβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) & β’ (π β (π β (π΄ + π΅)) = (π Ξ£g (π β (0...π) β¦ ((πCπ) Β· (((π β π) β π΄) Γ (π β π΅)))))) β β’ ((π β§ π) β ((π β (π΄ + π΅)) Γ π΅) = (π Ξ£g (π β (0...(π + 1)) β¦ ((πC(π β 1)) Β· ((((π + 1) β π) β π΄) Γ (π β π΅)))))) | ||
Theorem | srgbinomlem 20125* | Lemma for srgbinom 20126. Inductive step, analogous to binomlem 15780. (Contributed by AV, 24-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ Β· = (.gβπ ) & β’ + = (+gβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) & β’ (π β (π β (π΄ + π΅)) = (π Ξ£g (π β (0...π) β¦ ((πCπ) Β· (((π β π) β π΄) Γ (π β π΅)))))) β β’ ((π β§ π) β ((π + 1) β (π΄ + π΅)) = (π Ξ£g (π β (0...(π + 1)) β¦ (((π + 1)Cπ) Β· ((((π + 1) β π) β π΄) Γ (π β π΅)))))) | ||
Theorem | srgbinom 20126* | The binomial theorem for commuting elements of a semiring: (π΄ + π΅)βπ is the sum from π = 0 to π of (πCπ) Β· ((π΄βπ) Β· (π΅β(π β π)) (generalization of binom 15781). (Contributed by AV, 24-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ Β· = (.gβπ ) & β’ + = (+gβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) β β’ (((π β SRing β§ π β β0) β§ (π΄ β π β§ π΅ β π β§ (π΄ Γ π΅) = (π΅ Γ π΄))) β (π β (π΄ + π΅)) = (π Ξ£g (π β (0...π) β¦ ((πCπ) Β· (((π β π) β π΄) Γ (π β π΅)))))) | ||
Theorem | csrgbinom 20127* | The binomial theorem for commutative semirings. (Contributed by AV, 24-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ Β· = (.gβπ ) & β’ + = (+gβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) β β’ (((π β SRing β§ πΊ β CMnd β§ π β β0) β§ (π΄ β π β§ π΅ β π)) β (π β (π΄ + π΅)) = (π Ξ£g (π β (0...π) β¦ ((πCπ) Β· (((π β π) β π΄) Γ (π β π΅)))))) | ||
Syntax | crg 20128 | Extend class notation with class of all (unital) rings. |
class Ring | ||
Syntax | ccrg 20129 | Extend class notation with class of all (unital) commutative rings. |
class CRing | ||
Definition | df-ring 20130* | Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition 1 in [BourbakiAlg1] p. 92 or definition of a ring with identity in part Preliminaries of [Roman] p. 19. So that the additive structure must be abelian (see ringcom 20169), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. Therefore, it can be shown that a unital ring is a non-unital ring (ringrng 20174) only after ringabl 20170 was proven. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ Ring = {π β Grp β£ ((mulGrpβπ) β Mnd β§ [(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘]βπ₯ β π βπ¦ β π βπ§ β π ((π₯π‘(π¦ππ§)) = ((π₯π‘π¦)π(π₯π‘π§)) β§ ((π₯ππ¦)π‘π§) = ((π₯π‘π§)π(π¦π‘π§))))} | ||
Definition | df-cring 20131 | Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ CRing = {π β Ring β£ (mulGrpβπ) β CMnd} | ||
Theorem | isring 20132* | The predicate "is a (unital) ring". Definition of "ring with unit" in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β (π β Grp β§ πΊ β Mnd β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ ((π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β§ ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))))) | ||
Theorem | ringgrp 20133 | A ring is a group. (Contributed by NM, 15-Sep-2011.) |
β’ (π β Ring β π β Grp) | ||
Theorem | ringmgp 20134 | A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ πΊ = (mulGrpβπ ) β β’ (π β Ring β πΊ β Mnd) | ||
Theorem | iscrng 20135 | A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ πΊ = (mulGrpβπ ) β β’ (π β CRing β (π β Ring β§ πΊ β CMnd)) | ||
Theorem | crngmgp 20136 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ πΊ = (mulGrpβπ ) β β’ (π β CRing β πΊ β CMnd) | ||
Theorem | ringgrpd 20137 | A ring is a group. (Contributed by SN, 16-May-2024.) |
β’ (π β π β Ring) β β’ (π β π β Grp) | ||
Theorem | ringmnd 20138 | A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ (π β Ring β π β Mnd) | ||
Theorem | ringmgm 20139 | A ring is a magma. (Contributed by AV, 31-Jan-2020.) |
β’ (π β Ring β π β Mgm) | ||
Theorem | crngring 20140 | A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ (π β CRing β π β Ring) | ||
Theorem | crngringd 20141 | A commutative ring is a ring. (Contributed by SN, 16-May-2024.) |
β’ (π β π β CRing) β β’ (π β π β Ring) | ||
Theorem | crnggrpd 20142 | A commutative ring is a group. (Contributed by SN, 16-May-2024.) |
β’ (π β π β CRing) β β’ (π β π β Grp) | ||
Theorem | mgpf 20143 | Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ (mulGrp βΎ Ring):RingβΆMnd | ||
Theorem | ringdilem 20144 | Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π Β· (π + π)) = ((π Β· π) + (π Β· π)) β§ ((π + π) Β· π) = ((π Β· π) + (π Β· π)))) | ||
Theorem | ringcl 20145 | Closure of the multiplication operation of a ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π΅) β (π Β· π) β π΅) | ||
Theorem | crngcom 20146 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ π β π΅ β§ π β π΅) β (π Β· π) = (π Β· π)) | ||
Theorem | iscrng2 20147* | A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β CRing β (π β Ring β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ Β· π¦) = (π¦ Β· π₯))) | ||
Theorem | ringass 20148 | Associative law for multiplication in a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π Β· π) Β· π) = (π Β· (π Β· π))) | ||
Theorem | ringideu 20149* | The unity element of a ring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β β!π’ β π΅ βπ₯ β π΅ ((π’ Β· π₯) = π₯ β§ (π₯ Β· π’) = π₯)) | ||
Theorem | crngbascntr 20150 | The base set of a commutative ring is its center. (Contributed by SN, 21-Mar-2025.) |
β’ π΅ = (BaseβπΊ) & β’ π = (Cntrβ(mulGrpβπΊ)) β β’ (πΊ β CRing β π΅ = π) | ||
Theorem | ringassd 20151 | Associative law for multiplication in a ring. (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π Β· π) Β· π) = (π Β· (π Β· π))) | ||
Theorem | ringcld 20152 | Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· π) β π΅) | ||
Theorem | ringdi 20153 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π Β· (π + π)) = ((π Β· π) + (π Β· π))) | ||
Theorem | ringdir 20154 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) Β· π) = ((π Β· π) + (π Β· π))) | ||
Theorem | ringidcl 20155 | The unity element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β 1 β π΅) | ||
Theorem | ring0cl 20156 | The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β 0 β π΅) | ||
Theorem | ringidmlem 20157 | Lemma for ringlidm 20158 and ringridm 20159. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β (( 1 Β· π) = π β§ (π Β· 1 ) = π)) | ||
Theorem | ringlidm 20158 | The unity element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β ( 1 Β· π) = π) | ||
Theorem | ringridm 20159 | The unity element of a ring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β (π Β· 1 ) = π) | ||
Theorem | isringid 20160* | Properties showing that an element πΌ is the unity element of a ring. (Contributed by NM, 7-Aug-2013.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β ((πΌ β π΅ β§ βπ₯ β π΅ ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯)) β 1 = πΌ)) | ||
Theorem | ringlidmd 20161 | The unity element of a ring is a left multiplicative identity. (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β ( 1 Β· π) = π) | ||
Theorem | ringridmd 20162 | The unity element of a ring is a right multiplicative identity. (Contributed by SN, 14-Aug-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β (π Β· 1 ) = π) | ||
Theorem | ringid 20163* | The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅) β βπ’ β π΅ ((π’ Β· π) = π β§ (π Β· π’) = π)) | ||
Theorem | ringo2times 20164 | A ring element plus itself is two times the element. "Two" in an arbitrary unital ring is the sum of the unity element with itself. (Contributed by AV, 24-Aug-2021.) Variant of o2timesd 20105 for rings. (Revised by AV, 5-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π΄ β π΅) β (π΄ + π΄) = (( 1 + 1 ) Β· π΄)) | ||
Theorem | ringadd2 20165* | A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.) (Proof shortened by AV, 1-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅) β βπ₯ β π΅ (π + π) = ((π₯ + π₯) Β· π)) | ||
Theorem | ringidss 20166 | A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π = ((mulGrpβπ ) βΎs π΄) & β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π΄ β π΅ β§ 1 β π΄) β 1 = (0gβπ)) | ||
Theorem | ringacl 20167 | Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π΅) β (π + π) β π΅) | ||
Theorem | ringcomlem 20168 | Lemma for ringcom 20169. This (formerly) part of the proof for ringcom 20169 is also applicable for semirings (without using the commutativity of the addition given per definition of a semiring), see srgcom4lem 20108. (Contributed by GΓ©rard Lang, 4-Dec-2014.) Variant of rglcom4d 20106 for rings. (Revised by AV, 5-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π΅) β ((π + π) + (π + π)) = ((π + π) + (π + π))) | ||
Theorem | ringcom 20169 | Commutativity of the additive group of a ring. (See also lmodcom 20663.) This proof requires the existence of a multiplicative identity, and the existence of additive inverses. Therefore, this proof is not applicable for semirings. (Contributed by GΓ©rard Lang, 4-Dec-2014.) (Proof shortened by AV, 1-Feb-2025.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) | ||
Theorem | ringabl 20170 | A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.) |
β’ (π β Ring β π β Abel) | ||
Theorem | ringcmn 20171 | A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ (π β Ring β π β CMnd) | ||
Theorem | ringabld 20172 | A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) |
β’ (π β π β Ring) β β’ (π β π β Abel) | ||
Theorem | ringcmnd 20173 | A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
β’ (π β π β Ring) β β’ (π β π β CMnd) | ||
Theorem | ringrng 20174 | A unital ring is a non-unital ring. (Contributed by AV, 6-Jan-2020.) |
β’ (π β Ring β π β Rng) | ||
Theorem | ringssrng 20175 | The unital rings are non-unital rings. (Contributed by AV, 20-Mar-2020.) |
β’ Ring β Rng | ||
Theorem | isringrng 20176* | The predicate "is a unital ring" as extension of the predicate "is a non-unital ring". (Contributed by AV, 17-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β (π β Rng β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π¦ β§ (π¦ Β· π₯) = π¦))) | ||
Theorem | ringpropd 20177* | 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 20178* | 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 20179 | 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 20180* | Properties that determine a ring. (Contributed by NM, 2-Aug-2013.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β π β Grp) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ (π β 1 β π΅) & β’ ((π β§ π₯ β π΅) β ( 1 Β· π₯) = π₯) & β’ ((π β§ π₯ β π΅) β (π₯ Β· 1 ) = π₯) β β’ (π β π β Ring) | ||
Theorem | iscrngd 20181* | Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β π β Grp) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ (π β 1 β π΅) & β’ ((π β§ π₯ β π΅) β ( 1 Β· π₯) = π₯) & β’ ((π β§ π₯ β π΅) β (π₯ Β· 1 ) = π₯) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) = (π¦ Β· π₯)) β β’ (π β π β CRing) | ||
Theorem | ringlz 20182 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (Proof shortened by AV, 30-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β ( 0 Β· π) = 0 ) | ||
Theorem | ringrz 20183 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (Proof shortened by AV, 30-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β (π Β· 0 ) = 0 ) | ||
Theorem | ringlzd 20184 | The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β ( 0 Β· π) = 0 ) | ||
Theorem | ringrzd 20185 | The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β (π Β· 0 ) = 0 ) | ||
Theorem | ringsrg 20186 | Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ (π β Ring β π β SRing) | ||
Theorem | ring1eq0 20187 | 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 20188 | 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 20189* | 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 20190* | 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 20191 | Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 37113 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β ((πβ 1 ) Β· π) = (πβπ)) | ||
Theorem | ringnegr 20192 | Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 37114 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β (π Β· (πβ 1 )) = (πβπ)) | ||
Theorem | ringmneg1 20193 | Negation of a product in a ring. (mulneg1 11655 analog.) Compared with rngmneg1 20062, the proof is shorter making use of the existence of a ring unity. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβπ) Β· π) = (πβ(π Β· π))) | ||
Theorem | ringmneg2 20194 | Negation of a product in a ring. (mulneg2 11656 analog.) Compared with rngmneg2 20063, the proof is shorter making use of the existence of a ring unity. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· (πβπ)) = (πβ(π Β· π))) | ||
Theorem | ringm2neg 20195 | Double negation of a product in a ring. (mul2neg 11658 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) (Proof shortened by AV, 30-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβπ) Β· (πβπ)) = (π Β· π)) | ||
Theorem | ringsubdi 20196 | Ring multiplication distributes over subtraction. (subdi 11652 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· (π β π)) = ((π Β· π) β (π Β· π))) | ||
Theorem | ringsubdir 20197 | Ring multiplication distributes over subtraction. (subdir 11653 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β π) Β· π) = ((π Β· π) β (π Β· π))) | ||
Theorem | mulgass2 20198 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.gβπ ) & β’ Γ = (.rβπ ) β β’ ((π β Ring β§ (π β β€ β§ π β π΅ β§ π β π΅)) β ((π Β· π) Γ π) = (π Β· (π Γ π))) | ||
Theorem | ring1 20199 | The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β β’ (π β π β π β Ring) | ||
Theorem | ringn0 20200 | Rings exist. (Contributed by AV, 29-Apr-2019.) |
β’ Ring β β |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |