RingQuot.neg_quot
theorem RingQuot.neg_quot :
∀ {R : Type uR} [inst : Ring R] (r : R → R → Prop) {a : R},
-{ toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (-a) }
This theorem states that for any given ring `R` and binary relation `r` on `R`, the negation of a quotient ring element `{ toQuot := Quot.mk (RingQuot.Rel r) a }` is equal to the quotient ring element created by negating `a` first `{ toQuot := Quot.mk (RingQuot.Rel r) (-a) }`. In simpler terms, the negation operation can be performed either before or after creating the quotient ring element, yielding the same result.
More concisely: For any ring `R` and binary relation `r`, the negation of a quotient ring element `{toQuot := Quot.mk (RingQuot.Rel r) a}` is equal to the quotient ring element created by negating `a` first, i.e., `{toQuot := Quot.mk (RingQuot.Rel r) (-a)}`.
|
Mathlib.Algebra.RingQuot._auxLemma.2
theorem Mathlib.Algebra.RingQuot._auxLemma.2 :
∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop), 1 = { toQuot := Quot.mk (RingQuot.Rel r) 1 }
This theorem, named `_auxLemma.2` in the `Mathlib.Algebra.RingQuot` module, states that for any type `R` equipped with a semiring structure, and any binary relation `r` on `R`, the numeral `1` is equal to the ring quotient object constructed from the equivalence class of `1` under the relation `RingQuot.Rel r`. This essentially shows that the representation of `1` as a ring quotient under any relation `r` corresponds to the numeral `1` itself.
More concisely: For any semiring `R` and relation `r` on `R`, the equivalence class of `1` in the quotient object `RingQuot.RingQuot.mk (RingQuot.Rel r) R 1` equals `1`.
|
RingQuot.mul_quot
theorem RingQuot.mul_quot :
∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop) {a b : R},
{ toQuot := Quot.mk (RingQuot.Rel r) a } * { toQuot := Quot.mk (RingQuot.Rel r) b } =
{ toQuot := Quot.mk (RingQuot.Rel r) (a * b) }
This theorem, `RingQuot.mul_quot`, states that for any semiring `R` and any binary relation `r` on `R`, the product of two quotient elements created by `Quot.mk` (which constructs a new quotient type), where the original elements are `a` and `b` from `R`, is equal to the quotient element created from the product `a * b` in `R`. In simple terms, it shows that multiplication in the original semiring `R` corresponds to multiplication in the quotient ring determined by the relation `r`.
More concisely: For any semiring `R` and binary relation `r` on `R`, `Quot.mk (a : R) (b : R) * Quot.mk (c : R) (d : R) = Quot.mk (a * c) (b * d)` in the quotient ring determined by `r`.
|
RingQuot.smul_quot
theorem RingQuot.smul_quot :
∀ {R : Type uR} [inst : Semiring R] {S : Type uS} [inst_1 : CommSemiring S] (r : R → R → Prop)
[inst_2 : Algebra S R] {n : S} {a : R},
n • { toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (n • a) }
This theorem states that for any semiring `R`, commutative semiring `S`, relation `r` on `R`, S-algebra structure on `R`, element `n` in `S`, and element `a` in `R`, the result of scalar multiplication of `n` with the equivalence class of `a` (represented as `{ toQuot := Quot.mk (RingQuot.Rel r) a }`) under the ring quotient by `r` is the equivalence class of the result of scalar multiplication of `n` with `a` (represented as `{ toQuot := Quot.mk (RingQuot.Rel r) (n • a) }`). In simpler terms, scalar multiplication in `S` commutes with taking ring quotients in `R`.
More concisely: For any commutative semiring `S`, semiring `R`, relation `r` on `R`, S-algebra structure on `R`, element `n` in `S`, and element `a` in `R`, the equivalence classes of `n • a` and `n` times the equivalence class of `a` under the ring quotient by `r` are equal.
|
Mathlib.Algebra.RingQuot._auxLemma.1
theorem Mathlib.Algebra.RingQuot._auxLemma.1 :
∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop), 0 = { toQuot := Quot.mk (RingQuot.Rel r) 0 }
This theorem, `Mathlib.Algebra.RingQuot._auxLemma.1`, states that for any type `R` equipped with a semiring structure, and any binary relation `r` on `R`, the zero element of `R` is equivalent to the quotient type created by the equivalence class of the zero element under the ring quotient relation derived from `r`. In other words, `0` is equivalent to the set of all elements related to `0` by `r` in the ring quotient.
More concisely: For any semiring `R` and binary relation `r` on `R`, the zero element of `R` is equivalent to the quotient class of zeros in `R` under the ring quotient relation derived from `r`.
|
RingQuot.add_quot
theorem RingQuot.add_quot :
∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop) {a b : R},
{ toQuot := Quot.mk (RingQuot.Rel r) a } + { toQuot := Quot.mk (RingQuot.Rel r) b } =
{ toQuot := Quot.mk (RingQuot.Rel r) (a + b) }
This theorem states that for any semiring `R` and a binary relation `r` on `R`, the sum of two elements `a` and `b` in `R` after being mapped to the quotient ring is equivalent to the result obtained by first adding `a` and `b` in `R` and then mapping the sum to the quotient ring. In other words, the operation of addition commutes with the operation of taking quotients with respect to the ring quotient relation `RingQuot.Rel r`.
More concisely: For any semiring `R` and relation `r` on `R`, the addition operation in the quotient ring of `R` modulo `r` commutes with the quotient operation, i.e., `(a + b) % r = a % r + b % r` for all `a, b` in `R`.
|