doc-next-gen

Mathlib.RingTheory.Congruence.Defs

Module docstring

{"# Congruence relations on rings

This file defines congruence relations on rings, which extend Con and AddCon on monoids and additive monoids.

Most of the time you likely want to use the Ideal.Quotient API that is built on top of this.

Main Definitions

  • RingCon R: the type of congruence relations respecting + and *.
  • RingConGen r: the inductively defined smallest ring congruence relation containing a given binary relation.

TODO

  • Use this for RingQuot too.
  • Copy across more API from Con and AddCon in GroupTheory/Congruence.lean. ","### Basic notation

The basic algebraic notation, 0, 1, +, *, -, ^, descend naturally under the quotient ","### Algebraic structure

The operations above on the quotient by c : RingCon R preserve the algebraic structure of R. "}

RingCon structure
(R : Type*) [Add R] [Mul R] extends Con R, AddCon R
Full source 
/-- A congruence relation on a type with an addition and multiplication is an equivalence relation
which preserves both. -/
structure RingCon (R : Type*) [Add R] [Mul R] extends Con R, AddCon R where
Ring Congruence Relation
Informal description
A congruence relation on a ring (or more generally, a type with addition and multiplication) is an equivalence relation that preserves both the additive and multiplicative structures. That is, for a relation `c` on `R`, if `x₁ ≈ y₁` and `x₂ ≈ y₂` under `c`, then both `x₁ + x₂ ≈ y₁ + y₂` and `x₁ * x₂ ≈ y₁ * y₂` must hold.
RingConGen.Rel inductive
[Add R] [Mul R] (r : R → R → Prop) : R → R → Prop
Full source 
/-- The inductively defined smallest ring congruence relation containing a given binary
    relation. -/
inductive RingConGen.Rel [Add R] [Mul R] (r : R → R → Prop) : R → R → Prop
  | of : ∀ x y, r x y → RingConGen.Rel r x y
  | refl : ∀ x, RingConGen.Rel r x x
  | symm : ∀ {x y}, RingConGen.Rel r x y → RingConGen.Rel r y x
  | trans : ∀ {x y z}, RingConGen.Rel r x y → RingConGen.Rel r y z → RingConGen.Rel r x z
  | add : ∀ {w x y z}, RingConGen.Rel r w x → RingConGen.Rel r y z →
      RingConGen.Rel r (w + y) (x + z)
  | mul : ∀ {w x y z}, RingConGen.Rel r w x → RingConGen.Rel r y z →
      RingConGen.Rel r (w * y) (x * z)
Generating relation for ring congruence
Informal description
Given a binary relation `r` on a type `R` equipped with addition and multiplication, `RingConGen.Rel r` is the smallest congruence relation on `R` that contains `r`. This relation is defined inductively to preserve both the additive and multiplicative structures of `R`.
ringConGen definition
[Add R] [Mul R] (r : R → R → Prop) : RingCon R
Full source 
/-- The inductively defined smallest ring congruence relation containing a given binary
    relation. -/
def ringConGen [Add R] [Mul R] (r : R → R → Prop) : RingCon R where
  r := RingConGen.Rel r
  iseqv := ⟨RingConGen.Rel.refl, @RingConGen.Rel.symm _ _ _ _, @RingConGen.Rel.trans _ _ _ _⟩
  add' := RingConGen.Rel.add
  mul' := RingConGen.Rel.mul
Smallest ring congruence relation containing a given relation
Informal description
Given a type $R$ with addition and multiplication, and a binary relation $r$ on $R$, the function `ringConGen r` constructs the smallest ring congruence relation on $R$ that contains $r$. This relation is defined inductively to preserve both the additive and multiplicative structures of $R$.
RingCon.instFunLikeForallProp instance
: FunLike (RingCon R) R (R → Prop)
Full source 
/-- A coercion from a congruence relation to its underlying binary relation. -/
instance : FunLike (RingCon R) R (R → Prop) where
  coe c := c.r
  coe_injective' x y h := by
    rcases x with ⟨⟨x, _⟩, _⟩
    rcases y with ⟨⟨y, _⟩, _⟩
    congr!
    rw [Setoid.ext_iff, (show ⇑x = ⇑y from h)]
    simp
Function-Like Structure of Ring Congruence Relations
Informal description
For any type $R$ with addition and multiplication, a ring congruence relation $c$ on $R$ can be viewed as a function-like structure that maps elements of $R$ to predicates on $R$. This means that for any $x \in R$, the relation $c(x)$ is a predicate indicating which elements of $R$ are congruent to $x$ under $c$.
RingCon.coe_mk theorem
(s : Con R) (h) : ⇑(mk s h) = s
Full source 
@[simp]
theorem coe_mk (s : Con R) (h) : ⇑(mk s h) = s := rfl
Equality of Constructed Ring Congruence and its Multiplicative Component
Informal description
For any multiplicative congruence relation $s$ on a ring $R$ and any proof $h$ that $s$ preserves addition, the underlying relation of the constructed ring congruence relation `mk s h` is equal to $s$.
RingCon.rel_eq_coe theorem
: c.r = c
Full source 
theorem rel_eq_coe : c.r = c :=
  rfl
Equality of Underlying Relation and Ring Congruence
Informal description
For any ring congruence relation $c$ on a ring $R$, the underlying binary relation $c.r$ is equal to $c$ itself.
RingCon.toCon_coe_eq_coe theorem
: (c.toCon : R → R → Prop) = c
Full source 
@[simp]
theorem toCon_coe_eq_coe : (c.toCon : R → R → Prop) = c :=
  rfl
Equality of Ring Congruence and its Multiplicative Component
Informal description
For any ring congruence relation $c$ on a ring $R$, the underlying multiplicative congruence relation (accessed via `c.toCon`) has the same predicate representation as $c$ itself. In other words, the equivalence relation induced by the multiplicative part of $c$ is identical to $c$ as a binary relation on $R$.
RingCon.refl theorem
(x) : c x x
Full source 
protected theorem refl (x) : c x x :=
  c.refl' x
Reflexivity of Ring Congruence Relations
Informal description
For any ring congruence relation $c$ on a ring $R$ and any element $x \in R$, the relation $c$ is reflexive at $x$, i.e., $x$ is congruent to itself under $c$.
RingCon.symm theorem
{x y} : c x y → c y x
Full source 
protected theorem symm {x y} : c x y → c y x :=
  c.symm'
Symmetry of Ring Congruence Relations
Informal description
For any ring congruence relation $c$ on a ring $R$ and any elements $x, y \in R$, if $x$ is congruent to $y$ under $c$ (i.e., $c(x, y)$ holds), then $y$ is congruent to $x$ under $c$ (i.e., $c(y, x)$ holds).
RingCon.trans theorem
{x y z} : c x y → c y z → c x z
Full source 
protected theorem trans {x y z} : c x y → c y z → c x z :=
  c.trans'
Transitivity of Ring Congruence Relations
Informal description
For any ring congruence relation $c$ on a ring $R$ and any elements $x, y, z \in R$, if $x \sim y$ and $y \sim z$ under $c$, then $x \sim z$ under $c$.
RingCon.add theorem
{w x y z} : c w x → c y z → c (w + y) (x + z)
Full source 
protected theorem add {w x y z} : c w x → c y z → c (w + y) (x + z) :=
  c.add'
Addition Preserves Ring Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$ and any elements $w, x, y, z \in R$, if $w \sim x$ and $y \sim z$ under $c$, then $w + y \sim x + z$ under $c$.
RingCon.mul theorem
{w x y z} : c w x → c y z → c (w * y) (x * z)
Full source 
protected theorem mul {w x y z} : c w x → c y z → c (w * y) (x * z) :=
  c.mul'
Multiplication Preserves Ring Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$ and any elements $w, x, y, z \in R$, if $w \sim x$ and $y \sim z$ under $c$, then $w * y \sim x * z$ under $c$.
RingCon.sub theorem
{S : Type*} [AddGroup S] [Mul S] (t : RingCon S) {a b c d : S} (h : t a b) (h' : t c d) : t (a - c) (b - d)
Full source 
protected theorem sub {S : Type*} [AddGroup S] [Mul S] (t : RingCon S)
    {a b c d : S} (h : t a b) (h' : t c d) : t (a - c) (b - d) := t.toAddCon.sub h h'
Subtraction Preserves Ring Congruence Relation
Informal description
Let $S$ be a type with an additive group structure and a multiplication operation, and let $t$ be a ring congruence relation on $S$. For any elements $a, b, c, d \in S$ such that $a \sim b$ and $c \sim d$ under $t$, it follows that $a - c \sim b - d$ under $t$.
RingCon.neg theorem
{S : Type*} [AddGroup S] [Mul S] (t : RingCon S) {a b} (h : t a b) : t (-a) (-b)
Full source 
protected theorem neg {S : Type*} [AddGroup S] [Mul S] (t : RingCon S)
    {a b} (h : t a b) : t (-a) (-b) := t.toAddCon.neg h
Negation Preserves Ring Congruence Relation
Informal description
Let $S$ be a type with an additive group structure and a multiplication operation, and let $t$ be a ring congruence relation on $S$. For any elements $a, b \in S$ such that $a \sim b$ under $t$, it follows that $-a \sim -b$ under $t$.
RingCon.nsmul theorem
{S : Type*} [AddMonoid S] [Mul S] (t : RingCon S) (m : ℕ) {x y : S} (hx : t x y) : t (m • x) (m • y)
Full source 
protected theorem nsmul {S : Type*} [AddMonoid S] [Mul S] (t : RingCon S)
    (m : ℕ) {x y : S} (hx : t x y) : t (m • x) (m • y) := t.toAddCon.nsmul m hx
Scalar Multiplication Preserves Ring Congruence for Natural Numbers
Informal description
Let $S$ be a type equipped with an additive monoid structure and a multiplication operation, and let $t$ be a ring congruence relation on $S$. For any natural number $m$ and elements $x, y \in S$ such that $x \sim y$ under $t$, it follows that $m \cdot x \sim m \cdot y$ under $t$, where $\cdot$ denotes the scalar multiplication operation.
RingCon.zsmul theorem
{S : Type*} [AddGroup S] [Mul S] (t : RingCon S) (z : ℤ) {x y : S} (hx : t x y) : t (z • x) (z • y)
Full source 
protected theorem zsmul {S : Type*} [AddGroup S] [Mul S] (t : RingCon S)
    (z : ℤ) {x y : S} (hx : t x y) : t (z • x) (z • y) := t.toAddCon.zsmul z hx
Integer Scalar Multiplication Preserves Ring Congruence Relation
Informal description
Let $S$ be a type equipped with an additive group structure and a multiplication operation, and let $t$ be a ring congruence relation on $S$. For any integer $z$ and elements $x, y \in S$ such that $x \sim y$ under $t$, it follows that $z \cdot x \sim z \cdot y$ under $t$, where $\cdot$ denotes the integer scalar multiplication operation.
RingCon.instInhabited instance
: Inhabited (RingCon R)
Full source 
instance : Inhabited (RingCon R) :=
  ⟨ringConGen EmptyRelation⟩
Existence of Trivial Ring Congruence Relation
Informal description
For any type $R$ with addition and multiplication, there exists a trivial ring congruence relation on $R$.
RingCon.rel_mk theorem
{s : Con R} {h a b} : RingCon.mk s h a b ↔ s a b
Full source 
@[simp]
theorem rel_mk {s : Con R} {h a b} : RingCon.mkRingCon.mk s h a b ↔ s a b :=
  Iff.rfl
Equivalence of Ring Congruence Relation and Underlying Multiplicative Congruence Relation
Informal description
For any congruence relation `s` on a ring `R`, and any elements `a, b : R`, the ring congruence relation `RingCon.mk s h` relates `a` and `b` if and only if the underlying multiplicative congruence relation `s` relates `a` and `b`.
RingCon.ext' theorem
{c d : RingCon R} (H : ⇑c = ⇑d) : c = d
Full source 
/-- The map sending a congruence relation to its underlying binary relation is injective. -/
theorem ext' {c d : RingCon R} (H : ⇑c = ⇑d) : c = d := DFunLike.coe_injective H
Injectivity of Ring Congruence Relation Construction
Informal description
For any two ring congruence relations $c$ and $d$ on a ring $R$, if the underlying binary relations of $c$ and $d$ are equal (i.e., $c(x,y) = d(x,y)$ for all $x,y \in R$), then $c = d$.
RingCon.ext theorem
{c d : RingCon R} (H : ∀ x y, c x y ↔ d x y) : c = d
Full source 
/-- Extensionality rule for congruence relations. -/
@[ext]
theorem ext {c d : RingCon R} (H : ∀ x y, c x y ↔ d x y) : c = d :=
  ext' <| by ext; apply H
Extensionality of Ring Congruence Relations
Informal description
Two ring congruence relations $c$ and $d$ on a ring $R$ are equal if and only if they relate the same pairs of elements, i.e., for all $x, y \in R$, $c(x, y) \leftrightarrow d(x, y)$.
RingCon.comap definition
{R R' F : Type*} [Add R] [Add R'] [FunLike F R R'] [AddHomClass F R R'] [Mul R] [Mul R'] [MulHomClass F R R'] (J : RingCon R') (f : F) : RingCon R
Full source 
/--
Pulling back a `RingCon` across a ring homomorphism.
-/
def comap {R R' F : Type*} [Add R] [Add R']
    [FunLike F R R'] [AddHomClass F R R'] [Mul R] [Mul R'] [MulHomClass F R R']
    (J : RingCon R') (f : F) :
    RingCon R where
  __ := J.toCon.comap f (map_mul f)
  __ := J.toAddCon.comap f (map_add f)
Pullback of a ring congruence relation along a ring homomorphism
Informal description
Given rings (or more generally, types with addition and multiplication) $R$ and $R'$, and a ring homomorphism $f \colon R \to R'$, the pullback of a ring congruence relation $J$ on $R'$ along $f$ is the ring congruence relation on $R$ defined by $x \sim y$ if and only if $f(x) \sim f(y)$ under $J$. This relation preserves both the additive and multiplicative structures of $R$.
RingCon.Quotient definition
Full source 
/-- Defining the quotient by a congruence relation of a type with addition and multiplication. -/
protected def Quotient :=
  Quotient c.toSetoid
Quotient ring by a congruence relation
Informal description
The quotient of a ring (or more generally, a type with addition and multiplication) by a congruence relation `c`. This is defined as the quotient of the underlying setoid associated with `c`, where elements of `R` are identified if they are related by `c`.
RingCon.toQuotient definition
(r : R) : c.Quotient
Full source 
/-- The morphism into the quotient by a congruence relation -/
@[coe] def toQuotient (r : R) : c.Quotient :=
  @Quotient.mk'' _ c.toSetoid r
Canonical projection to quotient ring by congruence relation
Informal description
The canonical map from a ring (or more generally, a type with addition and multiplication) to its quotient by a congruence relation $c$, sending an element $r \in R$ to its equivalence class in the quotient.
RingCon.instCoeTCQuotient instance
: CoeTC R c.Quotient
Full source 
/-- Coercion from a type with addition and multiplication to its quotient by a congruence relation.

See Note [use has_coe_t]. -/
instance : CoeTC R c.Quotient :=
  ⟨toQuotient⟩
Canonical Projection to Quotient Ring by Congruence Relation
Informal description
For any type $R$ with addition and multiplication and a congruence relation $c$ on $R$, there is a canonical map from $R$ to its quotient $R/c$ that sends each element to its equivalence class under $c$.
RingCon.instDecidableEqQuotientOfDecidableCoeForallProp instance
[_d : ∀ a b, Decidable (c a b)] : DecidableEq c.Quotient
Full source 
/-- The quotient by a decidable congruence relation has decidable equality. -/
instance (priority := 500) [_d : ∀ a b, Decidable (c a b)] : DecidableEq c.Quotient :=
  inferInstanceAs (DecidableEq (Quotient c.toSetoid))
Decidable Equality for Quotient Rings by Decidable Congruence Relations
Informal description
For any ring congruence relation $c$ on a ring $R$ with decidable relation (i.e., for any $a, b \in R$ it is decidable whether $a \approx b$ under $c$), the quotient ring $R/c$ has decidable equality.
RingCon.quot_mk_eq_coe theorem
(x : R) : Quot.mk c x = (x : c.Quotient)
Full source 
@[simp]
theorem quot_mk_eq_coe (x : R) : Quot.mk c x = (x : c.Quotient) :=
  rfl
Equivalence Class Equals Canonical Projection in Quotient Ring
Informal description
For any element $x$ in a ring $R$ with a congruence relation $c$, the equivalence class of $x$ under $c$ (constructed via `Quot.mk`) is equal to the canonical projection of $x$ to the quotient ring $R/c$.
RingCon.eq theorem
{a b : R} : (a : c.Quotient) = (b : c.Quotient) ↔ c a b
Full source 
/-- Two elements are related by a congruence relation `c` iff they are represented by the same
element of the quotient by `c`. -/
@[simp]
protected theorem eq {a b : R} : (a : c.Quotient) = (b : c.Quotient) ↔ c a b :=
  Quotient.eq''
Equivalence of Projections in Quotient Ring by Congruence Relation
Informal description
For any elements $a$ and $b$ in a ring $R$ with a congruence relation $c$, the canonical projections of $a$ and $b$ to the quotient ring $R/c$ are equal if and only if $a$ and $b$ are related by $c$, i.e., $[a] = [b] \leftrightarrow a \approx b \text{ under } c$.
RingCon.instAddQuotient instance
: Add c.Quotient
Full source 
instance : Add c.Quotient := inferInstanceAs (Add c.toAddCon.Quotient)
Addition on Quotient Ring by Congruence Relation
Informal description
The quotient ring $R/c$ by a congruence relation $c$ on a ring $R$ inherits an addition operation from $R$, where the sum of two equivalence classes $[x]$ and $[y]$ is defined as $[x + y]$.
RingCon.coe_add theorem
(x y : R) : (↑(x + y) : c.Quotient) = ↑x + ↑y
Full source 
@[simp, norm_cast]
theorem coe_add (x y : R) : (↑(x + y) : c.Quotient) = ↑x + ↑y :=
  rfl
Additivity of Canonical Projection to Quotient Ring
Informal description
For any elements $x$ and $y$ in a ring $R$ with a congruence relation $c$, the canonical projection of their sum $x + y$ to the quotient ring $R/c$ equals the sum of their individual projections, i.e., $[x + y] = [x] + [y]$.
RingCon.instMulQuotient instance
: Mul c.Quotient
Full source 
instance : Mul c.Quotient := inferInstanceAs (Mul c.toCon.Quotient)
Multiplication on the Quotient Ring by a Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient $R/c$ inherits a multiplication operation defined by $[x] \cdot [y] = [x \cdot y]$, where $[x]$ denotes the equivalence class of $x \in R$ under $c$.
RingCon.coe_mul theorem
(x y : R) : (↑(x * y) : c.Quotient) = ↑x * ↑y
Full source 
@[simp, norm_cast]
theorem coe_mul (x y : R) : (↑(x * y) : c.Quotient) = ↑x * ↑y :=
  rfl
Multiplication Preservation in Quotient Ring by Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$ and any elements $x, y \in R$, the equivalence class of the product $x \cdot y$ in the quotient ring $R/c$ equals the product of the equivalence classes of $x$ and $y$ in $R/c$. In other words, $\overline{x \cdot y} = \overline{x} \cdot \overline{y}$ where $\overline{\cdot}$ denotes the canonical projection to the quotient ring.
RingCon.instZeroQuotient instance
: Zero c.Quotient
Full source 
instance : Zero c.Quotient := inferInstanceAs (Zero c.toAddCon.Quotient)
Additive Identity in the Quotient Ring by a Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient $R/c$ has a canonical additive identity element.
RingCon.coe_zero theorem
: (↑(0 : R) : c.Quotient) = 0
Full source 
@[simp, norm_cast]
theorem coe_zero : (↑(0 : R) : c.Quotient) = 0 :=
  rfl
Preservation of Zero in Quotient Ring by Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$, the image of the additive identity $0 \in R$ under the canonical projection to the quotient ring $R/c$ is equal to the additive identity in $R/c$, i.e., $\overline{0} = 0$.
RingCon.instOneQuotient instance
: One c.Quotient
Full source 
instance : One c.Quotient := inferInstanceAs (One c.toCon.Quotient)
Identity Element in the Quotient Ring by a Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient $R/c$ has a canonical multiplicative identity element.
RingCon.coe_one theorem
: (↑(1 : R) : c.Quotient) = 1
Full source 
@[simp, norm_cast]
theorem coe_one : (↑(1 : R) : c.Quotient) = 1 :=
  rfl
Preservation of multiplicative identity in quotient ring by congruence relation
Informal description
For a ring congruence relation $c$ on a ring $R$, the canonical projection of the multiplicative identity $1 \in R$ to the quotient ring $R/c$ is equal to the multiplicative identity in $R/c$, i.e., $\overline{1} = 1$.
RingCon.instNegQuotient instance
: Neg c.Quotient
Full source 
instance : Neg c.Quotient := inferInstanceAs (Neg c.toAddCon.Quotient)
Negation in the Quotient Ring by a Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient $R/c$ has a canonical negation operation.
RingCon.coe_neg theorem
(x : R) : (↑(-x) : c.Quotient) = -x
Full source 
@[simp, norm_cast]
theorem coe_neg (x : R) : (↑(-x) : c.Quotient) = -x :=
  rfl
Negation Commutes with Quotient Projection in Ring Congruence
Informal description
For any ring congruence relation $c$ on a ring $R$ and any element $x \in R$, the canonical projection of $-x$ to the quotient ring $R/c$ is equal to the negation of the projection of $x$, i.e., $\overline{-x} = -\overline{x}$.
RingCon.instSubQuotient instance
: Sub c.Quotient
Full source 
instance : Sub c.Quotient := inferInstanceAs (Sub c.toAddCon.Quotient)
Subtraction in the Quotient Ring by a Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient ring $R/c$ has a canonical subtraction operation.
RingCon.coe_sub theorem
(x y : R) : (↑(x - y) : c.Quotient) = x - y
Full source 
@[simp, norm_cast]
theorem coe_sub (x y : R) : (↑(x - y) : c.Quotient) = x - y :=
  rfl
Subtraction Commutes with Quotient Projection in Ring Congruence
Informal description
For any ring congruence relation $c$ on a ring $R$ and any elements $x, y \in R$, the canonical projection of $x - y$ to the quotient ring $R/c$ is equal to the difference of the projections of $x$ and $y$, i.e., $\overline{x - y} = \overline{x} - \overline{y}$.
RingCon.hasZSMul instance
: SMul ℤ c.Quotient
Full source 
instance hasZSMul : SMul ℤ c.Quotient := inferInstanceAs (SMul ℤ c.toAddCon.Quotient)
Integer Scalar Multiplication on Quotient Ring by Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient ring $R/c$ has a canonical scalar multiplication by integers, where $n \cdot [x] = [n \cdot x]$ for any $n \in \mathbb{Z}$ and $x \in R$.
RingCon.coe_zsmul theorem
(z : ℤ) (x : R) : (↑(z • x) : c.Quotient) = z • (x : c.Quotient)
Full source 
@[simp, norm_cast]
theorem coe_zsmul (z : ℤ) (x : R) : (↑(z • x) : c.Quotient) = z • (x : c.Quotient) :=
  rfl
Integer Scalar Multiplication Commutes with Quotient Projection
Informal description
For any integer $z$ and any element $x$ in a ring $R$ with a congruence relation $c$, the equivalence class of the scalar multiple $z \cdot x$ in the quotient ring $R/c$ is equal to the scalar multiple $z$ applied to the equivalence class of $x$ in $R/c$. In symbols, $[z \cdot x] = z \cdot [x]$.
RingCon.hasNSMul instance
: SMul ℕ c.Quotient
Full source 
instance hasNSMul : SMul ℕ c.Quotient := inferInstanceAs (SMul ℕ c.toAddCon.Quotient)
Natural Scalar Multiplication on Quotient Ring by Congruence Relation
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient ring $R/c$ has a canonical scalar multiplication by natural numbers, where $n \cdot [x] = [n \cdot x]$ for any $n \in \mathbb{N}$ and $x \in R$.
RingCon.coe_nsmul theorem
(n : ℕ) (x : R) : (↑(n • x) : c.Quotient) = n • (x : c.Quotient)
Full source 
@[simp, norm_cast]
theorem coe_nsmul (n : ℕ) (x : R) : (↑(n • x) : c.Quotient) = n • (x : c.Quotient) :=
  rfl
Natural Scalar Multiplication Commutes with Quotient Projection
Informal description
For any natural number $n$ and any element $x$ in a ring $R$ with a congruence relation $c$, the equivalence class of the scalar multiple $n \cdot x$ in the quotient ring $R/c$ is equal to the scalar multiple $n$ applied to the equivalence class of $x$ in $R/c$. In symbols, $[n \cdot x] = n \cdot [x]$.
RingCon.instPowQuotientNat instance
: Pow c.Quotient ℕ
Full source 
instance : Pow c.Quotient ℕ := inferInstanceAs (Pow c.toCon.Quotient ℕ)
Natural Power Operation on Quotient Rings by Congruence Relations
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient ring $R/c$ is equipped with a natural power operation, where for any equivalence class $[x] \in R/c$ and natural number $n$, we define $[x]^n = [x^n]$.
RingCon.coe_pow theorem
(x : R) (n : ℕ) : (↑(x ^ n) : c.Quotient) = (x : c.Quotient) ^ n
Full source 
@[simp, norm_cast]
theorem coe_pow (x : R) (n : ℕ) : (↑(x ^ n) : c.Quotient) = (x : c.Quotient) ^ n :=
  rfl
Power Operation Commutes with Quotient by Ring Congruence
Informal description
For any ring congruence relation $c$ on a ring $R$, any element $x \in R$, and any natural number $n$, the equivalence class of $x^n$ in the quotient ring $R/c$ is equal to the $n$-th power of the equivalence class of $x$. In symbols: $$[x^n]_c = [x]_c^n$$ where $[\,\cdot\,]_c$ denotes the canonical projection $R \to R/c$.
RingCon.instNatCastQuotient instance
: NatCast c.Quotient
Full source 
instance : NatCast c.Quotient :=
  ⟨fun n => ↑(n : R)⟩
Natural Number Casting in Quotient Rings by Congruence Relations
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient ring $R/c$ inherits a natural number casting operation from $R$.
RingCon.coe_natCast theorem
(n : ℕ) : (↑(n : R) : c.Quotient) = n
Full source 
@[simp, norm_cast]
theorem coe_natCast (n : ℕ) : (↑(n : R) : c.Quotient) = n :=
  rfl
Preservation of Natural Numbers under Quotient by Ring Congruence
Informal description
For any natural number $n$ and any ring congruence relation $c$ on a ring $R$, the image of $n$ under the canonical projection $R \to R/c$ is equal to $n$ viewed as an element of the quotient ring $R/c$. In other words, the natural number $n$ is preserved under the quotient map.
RingCon.instIntCastQuotient instance
: IntCast c.Quotient
Full source 
instance : IntCast c.Quotient :=
  ⟨fun z => ↑(z : R)⟩
Integer Casting in Quotient Rings by Congruence Relations
Informal description
For any ring congruence relation $c$ on a ring $R$, the quotient ring $R/c$ inherits an integer casting operation from $R$.
RingCon.coe_intCast theorem
(n : ℕ) : (↑(n : R) : c.Quotient) = n
Full source 
@[simp, norm_cast]
theorem coe_intCast (n : ℕ) : (↑(n : R) : c.Quotient) = n :=
  rfl
Natural Number Casting in Quotient Ring Preserves Value
Informal description
For any natural number $n$ and any ring congruence relation $c$ on a ring $R$, the image of $n$ under the canonical projection from $R$ to the quotient ring $R/c$ is equal to $n$ itself, i.e., $\overline{n} = n$ in $R/c$.
RingCon.instInhabitedQuotient instance
[Inhabited R] [Add R] [Mul R] (c : RingCon R) : Inhabited c.Quotient
Full source 
instance [Inhabited R] [Add R] [Mul R] (c : RingCon R) : Inhabited c.Quotient :=
  ⟨↑(default : R)⟩
Inhabited Quotient of a Ring by a Congruence Relation
Informal description
For any ring $R$ with addition and multiplication operations, and any congruence relation $c$ on $R$, the quotient $R/c$ is inhabited (i.e., contains at least one element) if $R$ itself is inhabited.
RingCon.instNonUnitalNonAssocSemiringQuotient instance
[NonUnitalNonAssocSemiring R] (c : RingCon R) : NonUnitalNonAssocSemiring c.Quotient
Full source 
instance [NonUnitalNonAssocSemiring R] (c : RingCon R) :
    NonUnitalNonAssocSemiring c.Quotient := fast_instance%
  Function.Surjective.nonUnitalNonAssocSemiring _ Quotient.mk''_surjective rfl
    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Quotient of a Non-Unital Non-Associative Semiring by a Congruence Relation is a Non-Unital Non-Associative Semiring
Informal description
For any non-unital non-associative semiring $R$ and any ring congruence relation $c$ on $R$, the quotient $R/c$ inherits a non-unital non-associative semiring structure from $R$.
RingCon.instNonAssocSemiringQuotient instance
[NonAssocSemiring R] (c : RingCon R) : NonAssocSemiring c.Quotient
Full source 
instance [NonAssocSemiring R] (c : RingCon R) : NonAssocSemiring c.Quotient := fast_instance%
  Function.Surjective.nonAssocSemiring _ Quotient.mk''_surjective rfl rfl (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl
Quotient of a Non-Associative Semiring by a Congruence Relation is a Non-Associative Semiring
Informal description
For any non-associative semiring $R$ and any ring congruence relation $c$ on $R$, the quotient ring $R/c$ inherits a non-associative semiring structure from $R$.
RingCon.instNonUnitalSemiringQuotient instance
[NonUnitalSemiring R] (c : RingCon R) : NonUnitalSemiring c.Quotient
Full source 
instance [NonUnitalSemiring R] (c : RingCon R) : NonUnitalSemiring c.Quotient := fast_instance%
  Function.Surjective.nonUnitalSemiring _ Quotient.mk''_surjective rfl (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl
Quotient of a Non-Unital Semiring by a Congruence Relation is a Non-Unital Semiring
Informal description
For any non-unital semiring $R$ and any ring congruence relation $c$ on $R$, the quotient $R/c$ inherits a non-unital semiring structure from $R$.
RingCon.instSemiringQuotient instance
[Semiring R] (c : RingCon R) : Semiring c.Quotient
Full source 
instance [Semiring R] (c : RingCon R) : Semiring c.Quotient := fast_instance%
  Function.Surjective.semiring _ Quotient.mk''_surjective rfl rfl (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl
Quotient of a Semiring by a Congruence Relation is a Semiring
Informal description
For any semiring $R$ and any ring congruence relation $c$ on $R$, the quotient $R/c$ inherits a semiring structure from $R$.
RingCon.instCommSemiringQuotient instance
[CommSemiring R] (c : RingCon R) : CommSemiring c.Quotient
Full source 
instance [CommSemiring R] (c : RingCon R) : CommSemiring c.Quotient := fast_instance%
  Function.Surjective.commSemiring _ Quotient.mk''_surjective rfl rfl (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ => rfl
Quotient of a Commutative Semiring by a Congruence Relation is a Commutative Semiring
Informal description
For any commutative semiring $R$ and any ring congruence relation $c$ on $R$, the quotient $R/c$ inherits a commutative semiring structure from $R$.
RingCon.instNonUnitalNonAssocRingQuotient instance
[NonUnitalNonAssocRing R] (c : RingCon R) : NonUnitalNonAssocRing c.Quotient
Full source 
instance [NonUnitalNonAssocRing R] (c : RingCon R) :
    NonUnitalNonAssocRing c.Quotient := fast_instance%
  Function.Surjective.nonUnitalNonAssocRing _ Quotient.mk''_surjective rfl (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Quotient of a Non-Unital Non-Associative Ring by a Congruence Relation is a Non-Unital Non-Associative Ring
Informal description
For any non-unital non-associative ring $R$ and any ring congruence relation $c$ on $R$, the quotient $R/c$ inherits a non-unital non-associative ring structure from $R$.
RingCon.instNonAssocRingQuotient instance
[NonAssocRing R] (c : RingCon R) : NonAssocRing c.Quotient
Full source 
instance [NonAssocRing R] (c : RingCon R) : NonAssocRing c.Quotient := fast_instance%
  Function.Surjective.nonAssocRing _ Quotient.mk''_surjective rfl rfl (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ => rfl) fun _ => rfl
Quotient of a Non-Associative Ring by a Congruence Relation is a Non-Associative Ring
Informal description
For any non-associative ring $R$ and any ring congruence relation $c$ on $R$, the quotient $R/c$ inherits a non-associative ring structure from $R$.
RingCon.instNonUnitalRingQuotient instance
[NonUnitalRing R] (c : RingCon R) : NonUnitalRing c.Quotient
Full source 
instance [NonUnitalRing R] (c : RingCon R) : NonUnitalRing c.Quotient := fast_instance%
  Function.Surjective.nonUnitalRing _ Quotient.mk''_surjective rfl (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Quotient of a Non-Unital Ring by a Congruence Relation is a Non-Unital Ring
Informal description
For any non-unital ring $R$ and any ring congruence relation $c$ on $R$, the quotient $R/c$ inherits a non-unital ring structure from $R$.
RingCon.instRingQuotient instance
[Ring R] (c : RingCon R) : Ring c.Quotient
Full source 
instance [Ring R] (c : RingCon R) : Ring c.Quotient := fast_instance%
  Function.Surjective.ring _ Quotient.mk''_surjective rfl rfl (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl
Quotient of a Ring by a Congruence Relation is a Ring
Informal description
For any ring $R$ and any ring congruence relation $c$ on $R$, the quotient $R/c$ inherits a ring structure from $R$.
RingCon.instCommRingQuotient instance
[CommRing R] (c : RingCon R) : CommRing c.Quotient
Full source 
instance [CommRing R] (c : RingCon R) : CommRing c.Quotient := fast_instance%
  Function.Surjective.commRing _ Quotient.mk''_surjective rfl rfl (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl
Quotient of a Commutative Ring by a Congruence Relation is a Commutative Ring
Informal description
For any commutative ring $R$ and any ring congruence relation $c$ on $R$, the quotient ring $R/c$ inherits a commutative ring structure from $R$.
RingCon.mk' definition
[NonAssocSemiring R] (c : RingCon R) : R →+* c.Quotient
Full source 
/-- The natural homomorphism from a ring to its quotient by a congruence relation. -/
def mk' [NonAssocSemiring R] (c : RingCon R) : R →+* c.Quotient where
  toFun := toQuotient
  map_zero' := rfl
  map_one' := rfl
  map_add' _ _ := rfl
  map_mul' _ _ := rfl
Canonical projection to quotient ring by congruence relation
Informal description
The natural homomorphism from a non-associative semiring $R$ to its quotient by a congruence relation $c$, which maps each element $r \in R$ to its equivalence class in $R/c$. This homomorphism preserves the additive and multiplicative structures, sending $0$ to $\overline{0}$, $1$ to $\overline{1}$, $r_1 + r_2$ to $\overline{r_1 + r_2}$, and $r_1 \cdot r_2$ to $\overline{r_1 \cdot r_2}$.