nyuuzyou/wikis huggingface dataset:
Proof by Cases/Proof Rule/Technical Note

== Technical Note on ==
When invoking in a tableau proof, use the template:
:{{ProofByCases|line|pool|statement|base|start1|end1|start2|end2}}
where:
:line is the number of the line on the tableau proof where is to be invoked
:pool is the pool of assumptions (comma-separated list)
:statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
:base is the line of the tableau proof where the disjunction being eliminated is situated
:start1 is the start line of the block of the tableau proof upon which the demonstration of the first disjunct directly depends
:end1 is the end line of the block of the tableau proof upon which the demonstration of the first disjunct directly depends
:start2 is the start line of the block of the tableau proof upon which the demonstration of the second disjunct directly depends
:end2 is the end line of the block of the tableau proof upon which the demonstration of the second disjunct directly depends
Category:Technical Notes
Proof by Cases/Sequent Form/Proof 2

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
$\begin{array}{|ccc|ccc|ccc||c|} \hline
p & \lor & q & p & \implies & r & q & \implies & r & r \\
\hline
F & F & F & F & T & F & F & T & F & F \\
F & F & F & F & T & T & F & T & T & T \\
F & T & T & F & T & F & T & F & F & F \\
F & T & T & F & T & T & T & T & T & T \\
T & T & F & T & F & F & F & T & F & F \\
T & T & F & T & T & T & F & T & T & T \\
T & T & T & T & F & F & T & F & F & F \\
T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
As can be seen, when $p \lor q$, $p \implies r$ and $q \implies r$ are all true, then so is $r$.
Category:Truth Table Proofs
Category:Proof by Cases
Proof by Cases with Contradiction

== Theorem ==
:$\vdash p \iff \left({p \lor q}\right) \land \left({p \lor \neg q}\right)$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T69}$
Category:Principle of Non-Contradiction
Category:Proof by Cases
Proof by Contradiction

== Proof Rule ==
Proof by Contradiction is a valid argument in types of logic dealing with negation $\neg$ and contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
=== Proof Rule ===
=== Sequent Form ===
== Explanation ==
== Also known as ==
== Variants ==
The following forms can be used as variants of this theorem:
=== Variant 1 ===
=== Variant 2 ===
=== Variant 3 ===
== Also see ==
* Definition:Logical Not
* Definition:Contradiction
* Reductio ad Absurdum
* Law of Excluded Middle
== Sources ==
* 
* : Chapter $1$: Elementary, my dear Watson: $\S 1.1$: You have a logical mind if...
* 
* 
Category:Proof by Contradiction
Category:Logical Negation
Category:Contradiction
Category:Proof Techniques
Proof by Contradiction/Also known as

== Proof by Contradiction: Also known as ==
Proof by contradiction is also known as not-introduction, and can be seen abbreviated as $\neg \II$ or $\neg_i$.
However, there are technical reasons why this form of abbreviation are suboptimal on this website, and PBC (if abbreviation is needed at all) is to be preferred.
It is also known as proof of negation, that is, proof that some (positive!) assumption is not true.
Some sources do not explicitly distinguish between proof by contradiction and reductio ad absurdum, which starts with a negative assumption ($\neg \phi$).
Both can be referred to as indirect proof, but reductio ad absurdum is rejected by the intuitionistic school.
Category:Proof by Contradiction
Proof by Contradiction/Proof Rule

== Proof Rule ==
Proof by contradiction is a valid argument in types of logic dealing with negation $\neg$ and contradiction $\bot$.
This includes classical propositional logic and predicate logic, and in particular natural deduction.
As a proof rule it is expressed in the form:
:If, by making an assumption $\phi$, we can infer a contradiction as a consequence, then we may infer $\neg \phi$.
:The conclusion $\neg \phi$ does not depend upon the assumption $\phi$.
It can be written:
:$\ds {\begin{array}{|c|} \hline \phi \\ \vdots \\ \bot \\ \hline \end{array} \over \neg \phi} \ \textrm{PBC}$
=== Tableau Form ===
== Explanation ==
== Also known as ==
== Also see ==
* This is a rule of inference of the following proof systems:
** Definition:Natural Deduction
== Technical Note ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 3$
* : $\S \text{II}$: The Logic of Statements $(2): \ 8$: Indirect proof
* : $\S 1.2.1$: Rules for natural deduction
Category:Proof by Contradiction
Category:Rules of Inference
Proof by Contradiction/Proof Rule/Technical Note

== Technical Note on ==
When invoking in a tableau proof, use the template:
:{{Contradiction|line|pool|statement|start|end}}
where:
:line is the number of the line on the tableau proof where the is to be invoked
:pool is the pool of assumptions (comma-separated list)
:statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
:start is the start of the block of the tableau proof upon which this line directly depends
:end is the end of the block of the tableau proof upon which this line directly depends
Category:Technical Notes
Proof by Contradiction/Variant 2/Formulation 1

== Theorem ==
:$p \implies q, p \implies \neg q \vdash \neg p$
== Proof ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 3$: Exercises, Group $\text{I}: \ 18$
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction: Theorem $22$
* : $\S 1.2.1$: Rules for natural deduction: Example $1.21$
Category:Proof by Contradiction
Proof by Contradiction/Variant 2/Formulation 2

== Theorem ==
:$\vdash \paren {\paren {p \implies q} \land \paren {p \implies \neg q} } \implies \neg p$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$: Theorem $\text{T34}$
Category:Proof by Contradiction
Proof by Contradiction/Variant 3/Formulation 1

== Theorem ==
:$p \implies \neg p \vdash \neg p$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction: Theorem $23$
* : $\S 1.2.1$: Rules for natural deduction: Example $1.21$
Category:Proof by Contradiction
Proof by Contradiction/Variant 3/Formulation 2

== Theorem ==
:$\vdash \paren {p \implies \neg p} \implies \neg p$
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 4.7$: The Derivation of Formulae: $\text D 1$
* : $\text{I}$: 'NOT' and 'IF': $\S 5$: Theorem $\text T20$
Category:Proof by Contradiction
Proof by Contradiction for Hilbert Proof System Instance 1 for Predicate Logic

== Theorem ==
Let $\LL$ be the language of predicate logic.
Let $\mathscr H$ be instance 1 of a Hilbert proof system for predicate logic.
Then Proof by Contradiction is a derived rule of $\mathscr H$:
== Proof ==
Suppose that $\Sigma, \phi \vdash_{\mathscr H} \bot$.
By Contradictory Antecedent, $\bot \implies \neg\phi$ is a tautology.
Therefore, $\bot \implies \neg\phi$ is an axiom of $\mathscr H$, so that by Modus Ponendo Ponens:
:$\Sigma, \phi \vdash_{\mathscr H} \neg \phi$
By Deduction Theorem for Hilbert Proof System for Predicate Logic, it follows that:
:$\Sigma \vdash_{\mathscr H} \phi \implies \neg \phi$
Next, note that $\paren {\phi \implies \neg \phi} \implies \neg \phi$ is a tautology and so an axiom of $\mathscr H$.
Hence by Modus Ponendo Ponens:
:$\Sigma \vdash_{\mathscr H} \neg \phi$
== Sources ==
* : $\text{II}.11$ Some Strategies for Constructing Proofs: Lemma $\text{II}.11.4$
Category:Proof by Contradiction
Category:Hilbert Proof System Instance 1 for Predicate Logic
Proof by Contraposition

== Proof Technique ==
Proof by Contraposition is a rule of inference used in proofs. 
This rule infers a conditional statement from its contrapositive.
It is based on the Rule of Transposition, which says that a conditional statement and its contrapositive have the same truth value:
:$p \implies q \dashv \vdash \neg q \implies \neg p$
In other words, the conclusion:
:if $A$, then $B$
is drawn from the single premise:
:if not $B$, then not $A$.
 
== Explanation ==
Proof by Contraposition can be expressed in natural language as follows:
If we know that by making an assumption 
:$\neg q$ 
we can deduce 
:$\neg p$
then it must be the case that 
:$p \implies q$.
Thus it provides a means of proving a logical implication.
== Examples ==
== Intuitionist Perspective ==
== Also known as ==
== Sources ==
* 
* 
Category:Proof by Contraposition
Category:Propositional Logic
Category:Proof Techniques
Proof by Contraposition/Also known as

== Proof by Contraposition: Also known as == 
The Proof by Contraposition is often confused with Reductio ad Absurdum, which also starts with an assumption $\neg q$.
To complicate things further, Reductio ad Absurdum itself is often confused with Proof by Contradiction.
Unlike Reductio ad Absurdum however, Proof by Contraposition is considered a valid proof in intuitionistic logic, as is Proof by Contradiction.
Category:Proof by Contraposition
Proof by Contraposition/Examples/If 2^n-1 is Prime then n is Prime

== Example of Proof by Contraposition ==
An example of a proof by contraposition would be as follows:
:Let $2^n - 1$ be prime.
:Then $n$ is prime.
This is proved by showing that:
:If $n$ is composite, then $2^n - 1$ is composite.
== Sources ==
* 
* 
Category:Proof by Contraposition
Proof by Contraposition/Intuitionist Perspective

== Proof by Contraposition: Intuitionist Perspective ==
Proof by Contraposition is often confused with Reductio ad Absurdum, which also starts with an assumption $\neg q$.
Reductio ad Absurdum itself is often confused with Proof by Contradiction.
Unlike Reductio ad Absurdum however, Proof by Contraposition can be a valid proof in intuitionistic logic, just like Proof by Contradiction.
Specifically, suppose:
:$p \implies q$
is true. 
Suppose furthermore that we have a proof of:
:$\neg q$.
Then if we had a proof of $p$, it could be turned into a proof of $q$.
This would imply
:$q \land \neg q$
which is impossible.
Therefore, it cannot be the case that $p$ is true.
That is:
:$\neg p$
However, now suppose:
:$\neg q \implies \neg p$
is true.
Suppose furthermore that we have a proof of $p$.
Then, if we were to find a proof of $\neg q$, it could be turned into a proof of $\neg p$.
This would imply:
:$p \land \neg p$
which is impossible.
Thus it is not possible to prove $\neg q$.
Now intuitionistic logic does not accept the Law of Excluded Middle.
That is, from an intuitionist perspective, knowing that a statement $q$ is not false does not automatically allow us to deduce that $q$ is actually true.
Under this assumption, we only know:
:$\neg \neg q$
Hence the rejection, by the intuitionist school of the Reductio ad Absurdum, but not the Proof by Contradiction.
Category:Proof by Contraposition
Proof by Counterexample

== Proof Technique ==
Consider the definition of a counterexample:
Proving, or disproving, a statement in the form of $X$ by establishing the truth or falsehood of a statement in the form of $Y$ is known as the technique of proof by counterexample.
== Sources ==
* : $\S 1.7$: Counterexamples
* : $\S 3$: Statements and conditions; quantifiers
* : Chapter $1$: Sets and mappings: $\S 1.1$: The need for logic
Category:Proof Techniques
Category:Logic
Proof of Theorem by Truth Table

== Theorem ==
Let $\phi$ be a propositional formula whose atoms are $p_1, p_2, \ldots, p_n$.
Let $l$ be the line number of any row in the truth table of $\phi$.
Let $\hat {p_i}$ be defined as:
:$\hat {p_i} = \begin{cases}
p_i & : \text {the entry in line } l \text { of } p_i \text { is } \T \\
\neg p_i & : \text {the entry in line } l \text { of } p_i \text { is } \F
\end{cases}$
for all $i$ such that $1 \le i \ne n$.
Then:
:$(1): \quad \hat {p_1}, \hat {p_2}, \ldots, \hat {p_n} \vdash \phi$ is provable if the entry for $\phi$ in line $l$ is $\T$
:$(2): \quad \hat {p_1}, \hat {p_2}, \ldots, \hat {p_n} \vdash \neg \phi$ is provable if the entry for $\phi$ in line $l$ is $\F$
== Proof ==
:$(1): \quad$ Suppose $\phi$ is an atom $p$.
Then we need to show that $p \vdash p$ and $\neg p \vdash \neg p$.
These are proved in one line in the proof of the Law of Identity.
:$(2): \quad$ Suppose $\phi$ is of the form $\neg \phi_1$.
There are two cases to consider:
Suppose $\phi$ evaluates to $\T$.
Category:Propositional Logic
Propagation of Light in Inhomogeneous Medium

== Theorem ==
Let $v: \R^3 \to \R$ be a real function.
Let $M$ be a 3-dimensional Euclidean space.
Let $\gamma:t \in \R \to M$ be a smooth curve embedded in $M$, where $t$ is time.
Denote its derivative time by $v$.
Suppose $M$ is filled with an optically inhomogeneous medium such that at each point speed of light is $v = \map v {x, y, z}$
Suppose $\map y x$ and $\map z x$ are real functions.
Let the light move according to Fermat's principle.
Then equations of motion have the following form:
:$\dfrac {\partial v} {\partial y} \dfrac {\sqrt {1 + y'^2 + z'^2} } {v^2} + \dfrac \d {\d x} \dfrac {y'} {v \sqrt {1 + y'^2 + z'^2} } = 0$
:$\dfrac {\partial v} {\partial z} \dfrac {\sqrt {1 + y'^2 + z'^2} } {v^2} + \dfrac \d {\d x} \dfrac {z'} {v \sqrt {1 + y'^2 + z'^2} } = 0$
== Proof ==
By assumption, $\map y x$ and $\map z x$ are real functions.
This allows us to $x$ instead of $t$ to parameterize the curve.
This reduces the number of equations of motion to $2$, that is: $\map y x$ and $\map z x$.
The time it takes to traverse the curve $\gamma$ equals:
According to Fermat's principle, light travels along the trajectory of least time.
Therefore, this integral has to be minimized $\map y x$ and $\map z x$.
It holds that:
:$\dfrac \partial {\partial y} \dfrac {\sqrt {1 + x'^2 + y'^2} } {\map v {x, y, z} } = -\dfrac {\sqrt {1 + x'^2 + y'^2} } {\map {v^2} {x, y, z} } \dfrac {\partial v} {\partial y}$
Also:
:$\dfrac \d {\d x} \dfrac \partial {\partial y'} \dfrac {\sqrt{1 + x'^2 + y'^2} } {\map v {x, y, z} } = \dfrac \d {\d x} \dfrac {y'} {v \sqrt {1 + x'^2 + y'^2} }$
Analogous relations hold for $\map z x$.
Then, by Euler's Equations and multiplication by $-1$, the desired result follows.
== Sources ==
* : $\S 2.9$: The Fixed End Point Problem for n Unknown Functions
Category:Calculus of Variations
Proper Class is not Element of Class

== Theorem ==
Let $\mathrm P$ be a proper class.
Then $\mathrm P$ is not an element of any class.
That is:
:$\neg \exists A : \mathrm P \in A$
== Proof ==
From the definition of a proper class, $\mathrm P$ is not a set.
The result follows by definition of a class.
Category:Class Theory
Proper Closed Linear Subspace of Topological Vector Space is Meager

== Theorem ==
Let $\GF \in \set {\R, \C}$.
Let $X$ be a topological vector space over $\GF$. 
Let $D$ be a proper closed linear subspace of $X$.
Then $D$ is meager.
== Proof ==
From Set is Closed iff Equals Topological Closure, we have $D^- = D$. 
From Proper Linear Subspace of Topological Vector Space has Empty Interior, we then have that $\paren {D^-}^\circ = D^\circ = \O$. 
Hence $D$ is nowhere dense, and in particular meager.
Category:Meager Spaces
Category:Topological Vector Spaces
Proper Filter is Included in Ultrafilter in Boolean Lattice

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a Boolean lattice.
Let $F$ be a proper filter on $L$.
Then there exists ultrafilter $G$ on $L$: $F \subseteq G$
== Proof ==
By Singleton of Bottom is Ideal:
:$I := \set \bot$ is an ideal in $L$.
where $\bot$ denotes the bottom of $L$.
We will prove that
:$F \cap I = \O$
Let $x \in I$.
By definition of singleton:
:$x = \bot$
Thus by Bottom not in Proper Filter:
:$x \notin F$
By If Ideal and Filter are Disjoint then There Exists Prime Filter Including Filter and Disjoint from Ideal:
:there exists a prime filter $G$ on $L$: $F \subseteq G$ and $G \cap I = \O$
By definition of singleton:
:$\bot \in I$
By definitions of empty set and intersection:
:$\bot \notin G$
By Bottom not in Proper Filter:
:$G$ is proper.
Thus by Proper and Prime iff Ultrafilter in Boolean Lattice:
:$G$ is ultrafilter.
Thus $F \subseteq G$
== Sources ==
* 
* 
Category:Order Theory
Proper Fraction/Examples

== Examples of Proper Fractions ==
=== Example: $\frac 3 4$ ===
=== Example: $\frac 7 8$ ===
=== Example: $\frac {-3} 4$ ===
=== Example: $\frac 6 {10}$ ===
=== Example: $\frac 3 2$ ===
Category:Examples of Proper Fractions
Proper Fraction can be Expressed as Finite Sum of Unit Fractions

== Theorem ==
Let $\dfrac p q$ denote a proper fraction expressed in canonical form.
Then it is always possible to express $\dfrac p q$ as the sum of a finite number of distinct unit fractions:
== Proof using Fibonacci's Greedy Algorithm ==
== Sources ==
* : Egyptian Fractions
Category:Unit Fractions
Category:Egyptian Fractions
Category:Proper Fraction can be Expressed as Finite Sum of Unit Fractions
Proper Fraction can be Expressed as Finite Sum of Unit Fractions/Fibonacci's Greedy Algorithm

== Theorem ==
== Proof: Fibonacci's Greedy Algorithm ==
We use Fibonacci's Greedy Algorithm:
The above constitutes an algorithm, for the following reasons:
=== Inputs ===
The input to this algorithm is the proper fraction $\dfrac p q$.
=== Definiteness ===
Steps $(1)$, $(2)$ and $(5)$ are trivially definite.
Step $(3)$:
We have:
while:
Hence $\dfrac 1 {\ceiling {y_k / x_k} }$ is the largest unit fraction less than $\dfrac {x_k} {y_k}$.
=== Finiteness ===
In order for the algorithm to terminate after a finite number of steps, at some stage step $(2)$ is to be executed where $x_m = 1$.
Hence it is to be shown that at the end of step $(4)$ $x_k = 1$ for some $k$.
We have:
We know that $x_k$ is not a divisor of $y_k$ as $\dfrac {x_k} {y_k}$ is expressed in canonical form.
Hence:
:$0 < \paren {-y_k} \bmod {x_k} < x_k$
Hence the numerator of $\dfrac {\paren {-y_k} \bmod {x_k} } {y_k \ceiling {y_k / x_k} }$ is strictly less than $x_k$.
Expressing $\dfrac {\paren {-y_k} \bmod {x_k} } {y_k \ceiling {y_k / x_k} }$ in the canonical form $\dfrac {x_{k + 1} } {y_{k + 1} }$ may reduce the numerator further, but will not increase it.
Hence:
:$x_{k + 1} < x_k$
and so by the Method of Infinite Descent it must eventually be the case that:
:$x_m = 1$
for some $m \in \N$.
=== Outputs ===
The output to this algorithm is the summation $\displaystyle \sum_{\substack {1 \mathop \le k \mathop \le m \\ n_j \mathop \le n_{j + 1} } } \dfrac 1 {n_k}$.
=== Effective ===
Each step of the algorithm is basic enough to be done exactly and in a finite length of time.
It is seen that every time step $(3)$ is executed, another unit fraction is generated.
When, at some stage after step $(4)$, $x_k = 1$, again a unit fraction has been generated.
But now it is not necessary to go through the algorithm again, and so at step $(2)$ the algorithm terminates.
It has output a sequence of unit fractions all of which have different denominators, which together add up to $\dfrac p q$.
All criteria are seen to hold.
The result follows.
== Sources ==
* 
* : Egyptian Fractions
Category:Proper Fraction can be Expressed as Finite Sum of Unit Fractions
Category:Fibonacci's Greedy Algorithm
Proper Ideal iff Quotient Ring is Non-Null

== Theorem ==
Let $A$ be a commutative ring.
Let $\mathfrak a \subseteq A$ be an ideal.
:$(1): \quad \mathfrak a$ is a proper ideal of $A$.
:$(2): \quad$ The quotient ring $A / \mathfrak a$ is a non-null ring.
== Proof ==
=== 1 implies 2 ===
Suppose $\mathfrak a$ is a proper ideal of $A$.
That is:
:$\exists x \in A \setminus \mathfrak a$
By definition of congruence modulo subgroup:
:$x + \mathfrak a \ne 0 + \mathfrak a$
in the quotient ring $A / \mathfrak a$.
Hence $A / \mathfrak a$ is a non-null ring.
=== 2 implies 1 ===
Suppose $A / \mathfrak a$ is a non-null ring.
That is:
:$\exists x, y \in A: x + \mathfrak a \ne y + \mathfrak a$
By definition of congruence modulo subgroup:
:$x - y \notin \mathfrak a$
Since $x - y \in A$:
:$\mathfrak a \ne A$
Hence $\mathfrak a$ is a proper ideal of $A$.
== Also see ==
* Proper Ideal of Ring is Contained in Maximal Ideal
Category:Quotient Rings
Proper Ideal is Prime iff Contains Element or Complement

== Theorem ==
Let $\struct {S, \preceq}$ be a boolean lattice.
Let $I$ be a proper ideal on $S$.
Then:
:$I$ is a prime ideal
:
:for every $a \in S$, either $a \in I$ or $\neg a \in I$.
== Proof ==
=== Necessary Condition ===
Suppose that $I$ is a prime ideal.
Then, by definition:
:$S \setminus I$ is a filter
 $a, \neg a \notin I$.
Then, $a, \neg \in S \setminus I$.
Hence, by Filter is Closed under Meet:
:$\neg a \wedge a \in S \setminus I$
but then by definition of complement:
:$\bot = \neg \wedge a \notin I$
which contradicts Bottom in Ideal.
=== Sufficient Condition ===
Suppose that for every $a \in S$:
:either $a \in I$ or $\neg a \in I$.
We will show that $S \setminus I$ satisfies the filter axioms.
As $I$ is a proper ideal:
:$I \subsetneq S$
and such:
:$S \setminus I \ne \O$
which is filter axiom $\paren 1$.
Let $x, y \in S \setminus I$.
Then, :
:$\neg x, \neg y \in I$
 $x \wedge y \in I$.
Hence:
But that is a contradiction by Top not in Proper Ideal.
Therefore, our assumption that:
:$x \wedge y \in I$
was false.
Therefore:
:$x \wedge y \in S \setminus I$
which is filter axiom $\paren 2$.
Finally, let:
:$x \in S \setminus I$
:$y \in S$
and suppose that:
:$x \preceq y$
If it were the case that:
:$y \in I$
we would have by ideal axiom $\paren 1$:
:$x \in I$
which is a contradiction.
Therefore, we must have:
:$y \in S \setminus I$
which is filter axiom $\paren 3$.
Category:Boolean Lattices
Category:Prime Ideals (Order Theory)
Proper Ideal of Ring is Contained in Maximal Ideal

== Theorem ==
Let $A$ be a commutative ring with unity.
Let $\mathfrak a \subseteq A$ be a proper ideal.
Then there exists a maximal ideal $\mathfrak m$ with $\mathfrak a \subseteq \mathfrak m$.
== Proof ==
Let $A / \mathfrak a$ be the quotient ring.
By Proper Ideal iff Quotient Ring is Non-Null, $A / \mathfrak a$ is non-null.
By Krull's Theorem, $A / \mathfrak a$ has a maximal ideal.
By Correspondence Theorem for Quotient Rings, $A$ has a maximal ideal containing $\mathfrak a$.
Category:Commutative Algebra
Category:Maximal Ideals of Rings