doc-next-gen

Mathlib.Algebra.Ring.InjSurj

Module docstring

{"# Pulling back rings along injective maps, and pushing them forward along surjective maps "}

Function.Injective.leftDistribClass theorem
[Mul R] [Add R] [LeftDistribClass R] (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass S
Full source 
/-- Pullback a `LeftDistribClass` instance along an injective function. -/
theorem leftDistribClass [Mul R] [Add R] [LeftDistribClass R] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass S where
  left_distrib x y z := hf <| by simp only [*, left_distrib]
Injective Pullback of Left Distributivity
Informal description
Let $R$ and $S$ be types equipped with multiplication and addition operations, and let $f : R \to S$ be an injective function. Suppose that $R$ satisfies the left distributive property (i.e., for all $a, b, c \in R$, $a \cdot (b + c) = a \cdot b + a \cdot c$). If $f$ preserves addition and multiplication (i.e., $f(x + y) = f(x) + f(y)$ and $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$), then $S$ also satisfies the left distributive property.
Function.Injective.rightDistribClass theorem
[Mul R] [Add R] [RightDistribClass R] (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) : RightDistribClass S
Full source 
/-- Pullback a `RightDistribClass` instance along an injective function. -/
theorem rightDistribClass [Mul R] [Add R] [RightDistribClass R] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : RightDistribClass S where
  right_distrib x y z := hf <| by simp only [*, right_distrib]
Injective Pullback of Right Distributivity
Informal description
Let $R$ and $S$ be types equipped with multiplication and addition operations, and let $f : R \to S$ be an injective function. Suppose that $R$ satisfies the right distributive property (i.e., for all $a, b, c \in R$, $(a + b) \cdot c = a \cdot c + b \cdot c$). If $f$ preserves addition and multiplication (i.e., $f(x + y) = f(x) + f(y)$ and $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$), then $S$ also satisfies the right distributive property.
Function.Injective.distrib abbrev
[Distrib R] (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) : Distrib S
Full source 
/-- Pullback a `Distrib` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev distrib [Distrib R] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : Distrib S where
  __ := hf.leftDistribClass f add mul
  __ := hf.rightDistribClass f add mul
Injective Pullback of Distributive Structure
Informal description
Given an injective function $f : R \to S$ between types $R$ and $S$, where $R$ has a distributive structure (i.e., multiplication distributes over addition), if $f$ preserves addition and multiplication (i.e., $f(x + y) = f(x) + f(y)$ and $f(x * y) = f(x) * f(y)$ for all $x, y \in R$), then $S$ inherits a distributive structure from $R$ via $f$.
Function.Injective.hasDistribNeg abbrev
(f : S → R) (hf : Injective f) [Mul R] [HasDistribNeg R] (neg : ∀ a, f (-a) = -f a) (mul : ∀ a b, f (a * b) = f a * f b) : HasDistribNeg S
Full source 
/-- A type endowed with `-` and `*` has distributive negation, if it admits an injective map that
preserves `-` and `*` to a type which has distributive negation. -/
-- -- See note [reducible non-instances]
protected abbrev hasDistribNeg (f : S → R) (hf : Injective f) [Mul R] [HasDistribNeg R]
    (neg : ∀ a, f (-a) = -f a)
    (mul : ∀ a b, f (a * b) = f a * f b) : HasDistribNeg S :=
  { hf.involutiveNeg _ neg, ‹Mul S› with
    neg_mul := fun x y => hf <| by rw [neg, mul, neg, neg_mul, mul],
    mul_neg := fun x y => hf <| by rw [neg, mul, neg, mul_neg, mul] }
Injective Pullback of Distributive Negation
Informal description
Let $S$ and $R$ be types with multiplication operations, and let $f : S \to R$ be an injective function. Suppose $R$ has distributive negation (i.e., $-a * b = -(a * b)$ and $a * -b = -(a * b)$ for all $a, b \in R$). If $f$ preserves negation and multiplication (i.e., $f(-a) = -f(a)$ and $f(a * b) = f(a) * f(b)$ for all $a, b \in S$), then $S$ also has distributive negation.
Function.Injective.nonUnitalNonAssocSemiring abbrev
[NonUnitalNonAssocSemiring R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocSemiring S
Full source 
/-- Pullback a `NonUnitalNonAssocSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocSemiring S where
  toAddCommMonoid := hf.addCommMonoid f zero add (swap nsmul)
  __ := hf.distrib f add mul
  __ := hf.mulZeroClass f zero mul
Injective Pullback of Non-unital Non-associative Semiring Structure
Informal description
Let $R$ be a non-unital non-associative semiring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$ - Multiplication: $f(x * y) = f(x) * f(y)$ for all $x, y \in S$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$ then $S$ inherits a non-unital non-associative semiring structure from $R$ via $f$.
Function.Injective.nonUnitalSemiring abbrev
[NonUnitalSemiring R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalSemiring S
Full source 
/-- Pullback a `NonUnitalSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalSemiring [NonUnitalSemiring R]
    (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) :
    NonUnitalSemiring S where
  toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
  __ := hf.semigroupWithZero f zero mul
Injective Pullback of Non-unital Semiring Structure
Informal description
Let $R$ be a non-unital semiring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x * y) = f(x) * f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, then $S$ inherits a non-unital semiring structure from $R$ via $f$.
Function.Injective.nonAssocSemiring abbrev
[NonAssocSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n) : NonAssocSemiring S
Full source 
/-- Pullback a `NonAssocSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonAssocSemiring [NonAssocSemiring R]
    (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (natCast : ∀ n : ℕ, f n = n) : NonAssocSemiring S where
  toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
  __ := hf.mulZeroOneClass f zero one mul
  __ := hf.addMonoidWithOne f zero one add nsmul natCast
Injective Pullback of Non-Associative Semiring Structure
Informal description
Let $R$ be a non-associative semiring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x * y) = f(x) * f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$, then $S$ inherits a non-associative semiring structure from $R$ via $f$.
Function.Injective.semiring abbrev
[Semiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : Semiring S
Full source 
/-- Pullback a `Semiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev semiring [Semiring R] (zero : f 0 = 0) (one : f 1 = 1)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) : Semiring S where
  toNonUnitalSemiring := hf.nonUnitalSemiring f zero add mul nsmul
  __ := hf.nonAssocSemiring f zero one add mul nsmul natCast
  __ := hf.monoidWithZero f zero one mul npow
Injective Pullback of Semiring Structure
Informal description
Let $R$ be a semiring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Natural number powers: $f(x^n) = f(x)^n$ for all $x \in S$ and $n \in \mathbb{N}$, - Natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$, then $S$ inherits a semiring structure from $R$ via $f$.
Function.Injective.nonUnitalNonAssocRing abbrev
[NonUnitalNonAssocRing R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocRing S
Full source 
/-- Pullback a `NonUnitalNonAssocRing` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocRing [NonUnitalNonAssocRing R] (f : S → R)
    (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
    (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocRing S where
  toAddCommGroup := hf.addCommGroup f zero add neg sub (swap nsmul) (swap zsmul)
  __ := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
Injective Pullback of Non-unital Non-associative Ring Structure
Informal description
Let $R$ be a non-unital non-associative ring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x * y) = f(x) * f(y)$ for all $x, y \in S$, - Negation: $f(-x) = -f(x)$ for all $x \in S$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in S$, then $S$ inherits a non-unital non-associative ring structure from $R$ via $f$.
Function.Injective.nonUnitalRing abbrev
[NonUnitalRing R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalRing S
Full source 
/-- Pullback a `NonUnitalRing` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalRing [NonUnitalRing R]
    (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) :
    NonUnitalRing S where
  toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
  __ := hf.nonUnitalSemiring f zero add mul nsmul
Injective Pullback of Non-unital Ring Structure
Informal description
Let $R$ be a non-unital ring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Negation: $f(-x) = -f(x)$ for all $x \in S$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in S$, then $S$ inherits a non-unital ring structure from $R$ via $f$.
Function.Injective.nonAssocRing abbrev
[NonAssocRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : NonAssocRing S
Full source 
/-- Pullback a `NonAssocRing` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonAssocRing [NonAssocRing R]
    (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
    (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n)
    (intCast : ∀ n : ℤ, f n = n) : NonAssocRing S where
  toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
  __ := hf.nonAssocSemiring f zero one add mul nsmul natCast
  __ := hf.addCommGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast
Injective Pullback of Non-Associative Ring Structure
Informal description
Let $R$ be a non-associative ring and $f \colon S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Negation: $f(-x) = -f(x)$ for all $x \in S$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in S$, - Natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$, - Integer casting: $f(n) = n$ for all $n \in \mathbb{Z}$, then $S$ inherits a non-associative ring structure from $R$ via $f$.
Function.Injective.ring abbrev
[Ring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : Ring S
Full source 
/-- Pullback a `Ring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev ring [Ring R] (zero : f 0 = 0)
    (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n)
    (intCast : ∀ n : ℤ, f n = n) : Ring S where
  toSemiring := hf.semiring f zero one add mul nsmul npow natCast
  __ := hf.addGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast
  __ := hf.addCommGroup f zero add neg sub (swap nsmul) (swap zsmul)
Injective Pullback of Ring Structure
Informal description
Let $R$ be a ring and $f \colon S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Negation: $f(-x) = -f(x)$ for all $x \in S$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in S$, - Natural number powers: $f(x^n) = f(x)^n$ for all $x \in S$ and $n \in \mathbb{N}$, - Natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$, - Integer casting: $f(n) = n$ for all $n \in \mathbb{Z}$, then $S$ inherits a ring structure from $R$ via $f$.
Function.Injective.nonUnitalNonAssocCommSemiring abbrev
[NonUnitalNonAssocCommSemiring R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocCommSemiring S
Full source 
/-- Pullback a `NonUnitalNonAssocCommSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocCommSemiring [NonUnitalNonAssocCommSemiring R]
    (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) :
    NonUnitalNonAssocCommSemiring S where
  toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
  __ := hf.commMagma f mul
Injective Pullback of Non-unital Non-associative Commutative Semiring Structure
Informal description
Let $R$ be a non-unital non-associative commutative semiring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$ then $S$ inherits a non-unital non-associative commutative semiring structure from $R$ via $f$.
Function.Injective.nonUnitalCommSemiring abbrev
[NonUnitalCommSemiring R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalCommSemiring S
Full source 
/-- Pullback a `NonUnitalCommSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalCommSemiring [NonUnitalCommSemiring R] (f : S → R)
    (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) :
    NonUnitalCommSemiring S where
  toNonUnitalSemiring := hf.nonUnitalSemiring f zero add mul nsmul
  __ := hf.commSemigroup f mul
Injective Pullback of Non-unital Commutative Semiring Structure
Informal description
Let $R$ be a non-unital commutative semiring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, then $S$ inherits a non-unital commutative semiring structure from $R$ via $f$.
Function.Injective.commSemiring abbrev
[CommSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : CommSemiring S
Full source 
/-- Pullback a `CommSemiring` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev commSemiring [CommSemiring R]
    (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) :
    CommSemiring S where
  toSemiring := hf.semiring f zero one add mul nsmul npow natCast
  __ := hf.commSemigroup f mul
Injective Pullback of Commutative Semiring Structure
Informal description
Let $R$ be a commutative semiring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Natural number powers: $f(x^n) = f(x)^n$ for all $x \in S$ and $n \in \mathbb{N}$, - Natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$, then $S$ inherits a commutative semiring structure from $R$ via $f$.
Function.Injective.nonUnitalNonAssocCommRing abbrev
[NonUnitalNonAssocCommRing R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocCommRing S
Full source 
/-- Pullback a `NonUnitalNonAssocCommRing` instance along an injective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocCommRing [NonUnitalNonAssocCommRing R] (f : S → R)
    (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
    (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocCommRing S where
  toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
  __ := hf.nonUnitalNonAssocCommSemiring f zero add mul nsmul
Injective Pullback of Non-unital Non-associative Commutative Ring Structure
Informal description
Let $R$ be a non-unital non-associative commutative ring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Negation: $f(-x) = -f(x)$ for all $x \in S$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in S$, then $S$ inherits a non-unital non-associative commutative ring structure from $R$ via $f$.
Function.Injective.nonUnitalCommRing abbrev
[NonUnitalCommRing R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalCommRing S
Full source 
/-- Pullback a `NonUnitalCommRing` instance along an injective function. -/
-- -- See note [reducible non-instances]
protected abbrev nonUnitalCommRing [NonUnitalCommRing R] (f : S → R)
    (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
    (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalCommRing S where
  toNonUnitalRing := hf.nonUnitalRing f zero add mul neg sub nsmul zsmul
  __ := hf.nonUnitalNonAssocCommRing f zero add mul neg sub nsmul zsmul
Injective Pullback of Non-unital Commutative Ring Structure
Informal description
Let $R$ be a non-unital commutative ring and $f : S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Negation: $f(-x) = -f(x)$ for all $x \in S$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in S$, then $S$ inherits a non-unital commutative ring structure from $R$ via $f$.
Function.Injective.commRing abbrev
[CommRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : CommRing S
Full source 
/-- Pullback a `CommRing` instance along an injective function. -/
-- -- See note [reducible non-instances]
protected abbrev commRing [CommRing R]
    (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
    (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : CommRing S where
  toRing := hf.ring f zero one add mul neg sub nsmul zsmul npow natCast intCast
  __ := hf.commMonoid f one mul npow
Injective Pullback of Commutative Ring Structure
Informal description
Let $R$ be a commutative ring and $f \colon S \to R$ be an injective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in S$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in S$, - Negation: $f(-x) = -f(x)$ for all $x \in S$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in S$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in S$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in S$, - Natural number powers: $f(x^n) = f(x)^n$ for all $x \in S$ and $n \in \mathbb{N}$, - Natural number casting: $f(n) = n$ for all $n \in \mathbb{N}$, - Integer casting: $f(n) = n$ for all $n \in \mathbb{Z}$, then $S$ inherits a commutative ring structure from $R$ via $f$.
Function.Surjective.leftDistribClass theorem
[Mul R] [Add R] [LeftDistribClass R] (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass S
Full source 
/-- Pushforward a `LeftDistribClass` instance along a surjective function. -/
theorem leftDistribClass [Mul R] [Add R] [LeftDistribClass R] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass S where
  left_distrib := hf.forall₃.2 fun x y z => by simp only [← add, ← mul, left_distrib]
Pushforward of Left Distributivity Along a Surjective Homomorphism
Informal description
Let $R$ be a type equipped with multiplication and addition operations that satisfy left distributivity, and let $f : R \to S$ be a surjective function. If $f$ preserves addition and multiplication, meaning that for all $x, y \in R$ we have $f(x + y) = f(x) + f(y)$ and $f(x \cdot y) = f(x) \cdot f(y)$, then $S$ inherits a left distributive structure from $R$ via $f$.
Function.Surjective.rightDistribClass theorem
[Mul R] [Add R] [RightDistribClass R] (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) : RightDistribClass S
Full source 
/-- Pushforward a `RightDistribClass` instance along a surjective function. -/
theorem rightDistribClass [Mul R] [Add R] [RightDistribClass R] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : RightDistribClass S where
  right_distrib := hf.forall₃.2 fun x y z => by simp only [← add, ← mul, right_distrib]
Pushforward of Right Distributivity Along a Surjective Homomorphism
Informal description
Let $R$ be a type equipped with multiplication and addition operations that satisfy right distributivity, and let $f : R \to S$ be a surjective function. If $f$ preserves addition and multiplication, meaning that for all $x, y \in R$ we have $f(x + y) = f(x) + f(y)$ and $f(x \cdot y) = f(x) \cdot f(y)$, then $S$ inherits a right distributive structure from $R$ via $f$.
Function.Surjective.distrib abbrev
[Distrib R] (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) : Distrib S
Full source 
/-- Pushforward a `Distrib` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev distrib [Distrib R] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : Distrib S where
  __ := hf.leftDistribClass f add mul
  __ := hf.rightDistribClass f add mul
Pushforward of Distributive Structure Along a Surjective Homomorphism
Informal description
Let $R$ be a type with a distributive structure (i.e., multiplication distributes over addition), and let $f : R \to S$ be a surjective function. If $f$ preserves addition and multiplication, meaning that for all $x, y \in R$ we have $f(x + y) = f(x) + f(y)$ and $f(x \cdot y) = f(x) \cdot f(y)$, then $S$ inherits a distributive structure from $R$ via $f$.
Function.Surjective.hasDistribNeg abbrev
[Mul R] [HasDistribNeg R] (neg : ∀ a, f (-a) = -f a) (mul : ∀ a b, f (a * b) = f a * f b) : HasDistribNeg S
Full source 
/-- A type endowed with `-` and `*` has distributive negation, if it admits a surjective map that
preserves `-` and `*` from a type which has distributive negation. -/
-- See note [reducible non-instances]
protected abbrev hasDistribNeg [Mul R] [HasDistribNeg R]
    (neg : ∀ a, f (-a) = -f a) (mul : ∀ a b, f (a * b) = f a * f b) : HasDistribNeg S :=
  { hf.involutiveNeg _ neg, ‹Mul S› with
    neg_mul := hf.forall₂.2 fun x y => by rw [← neg, ← mul, neg_mul, neg, mul]
    mul_neg := hf.forall₂.2 fun x y => by rw [← neg, ← mul, mul_neg, neg, mul] }
Pushforward of Distributive Negation Along a Surjective Homomorphism
Informal description
Let $R$ be a type with multiplication and distributive negation, and let $f : R \to S$ be a surjective function. If $f$ preserves negation and multiplication, i.e., for all $a \in R$, $f(-a) = -f(a)$, and for all $a, b \in R$, $f(a * b) = f(a) * f(b)$, then $S$ inherits a distributive negation structure from $R$ via $f$.
Function.Surjective.nonUnitalNonAssocSemiring abbrev
[NonUnitalNonAssocSemiring R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocSemiring S
Full source 
/-- Pushforward a `NonUnitalNonAssocSemiring` instance along a surjective function.
See note [reducible non-instances]. -/
protected abbrev nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocSemiring S where
  toAddCommMonoid := hf.addCommMonoid f zero add (swap nsmul)
  __ := hf.distrib f add mul
  __ := hf.mulZeroClass f zero mul
Pushforward of Non-Unital Non-Associative Semiring Structure Along a Surjective Homomorphism
Informal description
Let $R$ be a non-unital non-associative semiring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ then $S$ inherits a non-unital non-associative semiring structure from $R$ via $f$.
Function.Surjective.nonUnitalSemiring abbrev
[NonUnitalSemiring R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalSemiring S
Full source 
/-- Pushforward a `NonUnitalSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalSemiring [NonUnitalSemiring R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalSemiring S where
  toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
  __ := hf.semigroupWithZero f zero mul
Pushforward of Non-Unital Semiring Structure Along a Surjective Homomorphism
Informal description
Let $R$ be a non-unital semiring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ then $S$ inherits a non-unital semiring structure from $R$ via $f$.
Function.Surjective.nonAssocSemiring abbrev
[NonAssocSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n) : NonAssocSemiring S
Full source 
/-- Pushforward a `NonAssocSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonAssocSemiring [NonAssocSemiring R] (zero : f 0 = 0) (one : f 1 = 1)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (natCast : ∀ n : ℕ, f n = n) : NonAssocSemiring S where
  toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
  __ := hf.mulZeroOneClass f zero one mul
  __ := hf.addMonoidWithOne f zero one add nsmul natCast
Pushforward of Non-Associative Semiring Structure via Surjective Homomorphism
Informal description
Let $R$ be a non-associative semiring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$ - The multiplicative identity: $f(1) = 1$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ - The natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$ then $S$ inherits a non-associative semiring structure from $R$ via $f$.
Function.Surjective.semiring abbrev
[Semiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : Semiring S
Full source 
/-- Pushforward a `Semiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev semiring [Semiring R] (zero : f 0 = 0) (one : f 1 = 1)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : Semiring S where
  toNonUnitalSemiring := hf.nonUnitalSemiring f zero add mul nsmul
  __ := hf.nonAssocSemiring f zero one add mul nsmul natCast
  __ := hf.monoidWithZero f zero one mul npow
Pushforward of Semiring Structure via Surjective Homomorphism
Informal description
Let $R$ be a semiring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$, - Natural number powers: $f(x^n) = f(x)^n$ for all $x \in R$ and $n \in \mathbb{N}$, - The natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$, then $S$ inherits a semiring structure from $R$ via $f$.
Function.Surjective.nonUnitalNonAssocRing abbrev
[NonUnitalNonAssocRing R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocRing S
Full source 
/-- Pushforward a `NonUnitalNonAssocRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocRing [NonUnitalNonAssocRing R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) :
    NonUnitalNonAssocRing S where
  toAddCommGroup := hf.addCommGroup f zero add neg sub (swap nsmul) (swap zsmul)
  __ := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
Pushforward of Non-Unital Non-Associative Ring Structure via Surjective Homomorphism
Informal description
Let $R$ be a non-unital non-associative ring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - Negation: $f(-x) = -f(x)$ for all $x \in R$ - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in R$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in R$ then $S$ inherits a non-unital non-associative ring structure from $R$ via $f$.
Function.Surjective.nonUnitalRing abbrev
[NonUnitalRing R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalRing S
Full source 
/-- Pushforward a `NonUnitalRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalRing [NonUnitalRing R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) :
    NonUnitalRing S where
  toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
  __ := hf.nonUnitalSemiring f zero add mul nsmul
Pushforward of Non-Unital Ring Structure via Surjective Homomorphism
Informal description
Let $R$ be a non-unital ring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$, - Negation: $f(-x) = -f(x)$ for all $x \in R$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in R$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in R$, then $S$ inherits a non-unital ring structure from $R$ via $f$.
Function.Surjective.nonAssocRing abbrev
[NonAssocRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : NonAssocRing S
Full source 
/-- Pushforward a `NonAssocRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonAssocRing [NonAssocRing R] (zero : f 0 = 0) (one : f 1 = 1)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : NonAssocRing S where
  toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
  __ := hf.nonAssocSemiring f zero one add mul nsmul natCast
  __ := hf.addCommGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast
Pushforward of Non-Associative Ring Structure via Surjective Homomorphism
Informal description
Let $R$ be a non-associative ring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$ - The multiplicative identity: $f(1) = 1$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - Negation: $f(-x) = -f(x)$ for all $x \in R$ - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in R$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in R$ - The natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$ - The integer embedding: $f(n) = n$ for all $n \in \mathbb{Z}$ then $S$ inherits a non-associative ring structure from $R$ via $f$.
Function.Surjective.ring abbrev
[Ring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : Ring S
Full source 
/-- Pushforward a `Ring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev ring [Ring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n)
    (intCast : ∀ n : ℤ, f n = n) : Ring S where
  toSemiring := hf.semiring f zero one add mul nsmul npow natCast
  __ := hf.addGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast
  __ := hf.addCommGroup f zero add neg sub (swap nsmul) (swap zsmul)
Pushforward of Ring Structure via Surjective Homomorphism
Informal description
Let $R$ be a ring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$, - Negation: $f(-x) = -f(x)$ for all $x \in R$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in R$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in R$, - Natural number powers: $f(x^n) = f(x)^n$ for all $x \in R$ and $n \in \mathbb{N}$, - The natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$, - The integer embedding: $f(n) = n$ for all $n \in \mathbb{Z}$, then $S$ inherits a ring structure from $R$ via $f$.
Function.Surjective.nonUnitalNonAssocCommSemiring abbrev
[NonUnitalNonAssocCommSemiring R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocCommSemiring S
Full source 
/-- Pushforward a `NonUnitalNonAssocCommSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocCommSemiring  [NonUnitalNonAssocCommSemiring R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocCommSemiring S where
  toNonUnitalNonAssocSemiring := hf.nonUnitalNonAssocSemiring f zero add mul nsmul
  __ := hf.commMagma f mul
Pushforward of Non-Unital Non-Associative Commutative Semiring Structure Along a Surjective Homomorphism
Informal description
Let $R$ be a non-unital non-associative commutative semiring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ then $S$ inherits a non-unital non-associative commutative semiring structure from $R$ via $f$.
Function.Surjective.nonUnitalCommSemiring abbrev
[NonUnitalCommSemiring R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalCommSemiring S
Full source 
/-- Pushforward a `NonUnitalCommSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalCommSemiring [NonUnitalCommSemiring R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalCommSemiring S where
  toNonUnitalSemiring := hf.nonUnitalSemiring f zero add mul nsmul
  __ := hf.commSemigroup f mul
Pushforward of Non-Unital Commutative Semiring Structure via Surjective Homomorphism
Informal description
Let $R$ be a non-unital commutative semiring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ then $S$ inherits a non-unital commutative semiring structure from $R$ via $f$.
Function.Surjective.commSemiring abbrev
[CommSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : CommSemiring S
Full source 
/-- Pushforward a `CommSemiring` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev commSemiring [CommSemiring R] (zero : f 0 = 0) (one : f 1 = 1)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) : CommSemiring S where
  toSemiring := hf.semiring f zero one add mul nsmul npow natCast
  __ := hf.commSemigroup f mul
Pushforward of Commutative Semiring Structure via Surjective Homomorphism
Informal description
Let $R$ be a commutative semiring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$, - Natural number powers: $f(x^n) = f(x)^n$ for all $x \in R$ and $n \in \mathbb{N}$, - The natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$, then $S$ inherits a commutative semiring structure from $R$ via $f$.
Function.Surjective.nonUnitalNonAssocCommRing abbrev
[NonUnitalNonAssocCommRing R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocCommRing S
Full source 
/-- Pushforward a `NonUnitalNonAssocCommRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalNonAssocCommRing [NonUnitalNonAssocCommRing R]
    (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
    (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalNonAssocCommRing S where
  toNonUnitalNonAssocRing := hf.nonUnitalNonAssocRing f zero add mul neg sub nsmul zsmul
  __ := hf.nonUnitalNonAssocCommSemiring f zero add mul nsmul
Pushforward of Non-Unital Non-Associative Commutative Ring Structure via Surjective Homomorphism
Informal description
Let $R$ be a non-unital non-associative commutative ring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$ - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - Negation: $f(-x) = -f(x)$ for all $x \in R$ - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in R$ - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in R$ then $S$ inherits a non-unital non-associative commutative ring structure from $R$ via $f$.
Function.Surjective.nonUnitalCommRing abbrev
[NonUnitalCommRing R] (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) : NonUnitalCommRing S
Full source 
/-- Pushforward a `NonUnitalCommRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev nonUnitalCommRing [NonUnitalCommRing R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) :
    NonUnitalCommRing S where
  toNonUnitalRing := hf.nonUnitalRing f zero add mul neg sub nsmul zsmul
  __ := hf.nonUnitalNonAssocCommRing f zero add mul neg sub nsmul zsmul
Pushforward of Non-Unital Commutative Ring Structure via Surjective Homomorphism
Informal description
Let $R$ be a non-unital commutative ring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$, - Negation: $f(-x) = -f(x)$ for all $x \in R$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in R$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in R$, then $S$ inherits a non-unital commutative ring structure from $R$ via $f$.
Function.Surjective.commRing abbrev
[CommRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : CommRing S
Full source 
/-- Pushforward a `CommRing` instance along a surjective function. -/
-- See note [reducible non-instances]
protected abbrev commRing [CommRing R] (zero : f 0 = 0) (one : f 1 = 1)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : CommRing S where
  toRing := hf.ring f zero one add mul neg sub nsmul zsmul npow natCast intCast
  __ := hf.commMonoid f one mul npow
Pushforward of Commutative Ring Structure via Surjective Homomorphism
Informal description
Let $R$ be a commutative ring and $f : R \to S$ be a surjective function. If $f$ preserves: - The zero element: $f(0) = 0$, - The multiplicative identity: $f(1) = 1$, - Addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in R$, - Multiplication: $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$, - Negation: $f(-x) = -f(x)$ for all $x \in R$, - Subtraction: $f(x - y) = f(x) - f(y)$ for all $x, y \in R$, - Scalar multiplication by natural numbers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$, - Scalar multiplication by integers: $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in R$, - Natural number powers: $f(x^n) = f(x)^n$ for all $x \in R$ and $n \in \mathbb{N}$, - The natural number embedding: $f(n) = n$ for all $n \in \mathbb{N}$, - The integer embedding: $f(n) = n$ for all $n \in \mathbb{Z}$, then $S$ inherits a commutative ring structure from $R$ via $f$.
AddOpposite.instHasDistribNeg instance
: HasDistribNeg Rᵃᵒᵖ
Full source 
instance AddOpposite.instHasDistribNeg : HasDistribNeg Rᵃᵒᵖ :=
  unop_injective.hasDistribNeg _ unop_neg unop_mul
Distributive Negation on the Additive Opposite of a Ring
Informal description
The additive opposite $R^{\text{aop}}$ of a ring $R$ with distributive negation inherits a distributive negation structure, where the negation operation satisfies $-a * b = -(a * b)$ and $a * -b = -(a * b)$ for all $a, b \in R^{\text{aop}}$.