Pulling back rings along injective maps, and pushing them forward along surjective maps

theorem Function.Injective.leftDistribClass {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Mul R] [Add R] [LeftDistribClass R] (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) : LeftDistribClass S

Pullback a LeftDistribClass instance along an injective function.

theorem Function.Injective.rightDistribClass {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Mul R] [Add R] [RightDistribClass R] (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) : RightDistribClass S

Pullback a RightDistribClass instance along an injective function.

@[reducible, inline]

abbrev Function.Injective.distrib {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Distrib R] (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) : Distrib S

Pullback a Distrib instance along an injective function.

Equations

• Function.Injective.distrib f hf add mul = { toMul := inst✝¹, toAdd := inst✝², left_distrib := ⋯, right_distrib := ⋯ }

@[reducible, inline]

abbrev Function.Injective.hasDistribNeg {R : Type u_1} {S : Type u_2} [Mul S] [Neg S] (f : S → R) (hf : Injective f) [Mul R] [HasDistribNeg R] (neg : ∀ (a : S), f (-a) = -f a) (mul : ∀ (a b : S), f (a * b) = f a * f b) : HasDistribNeg S

A type endowed with - and * has distributive negation, if it admits an injective map that preserves - and * to a type which has distributive negation.

Equations

• Function.Injective.hasDistribNeg f hf neg mul = { toInvolutiveNeg := Function.Injective.involutiveNeg f hf neg, neg_mul := ⋯, mul_neg := ⋯ }

@[reducible, inline]

abbrev Function.Injective.nonUnitalNonAssocSemiring {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalNonAssocSemiring R] (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) : NonUnitalNonAssocSemiring S

Pullback a NonUnitalNonAssocSemiring instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.nonUnitalSemiring {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalSemiring R] (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) : NonUnitalSemiring S

Pullback a NonUnitalSemiring instance along an injective function.

Equations

• Function.Injective.nonUnitalSemiring f hf zero add mul nsmul = { toNonUnitalNonAssocSemiring := Function.Injective.nonUnitalNonAssocSemiring f hf zero add mul nsmul, mul_assoc := ⋯ }

@[reducible, inline]

abbrev Function.Injective.nonAssocSemiring {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [One S] [SMul ℕ S] [NatCast S] [NonAssocSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (natCast : ∀ (n : ℕ), f ↑n = ↑n) : NonAssocSemiring S

Pullback a NonAssocSemiring instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.semiring {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [One S] [SMul ℕ S] [Pow S ℕ] [NatCast S] [Semiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (npow : ∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) : Semiring S

Pullback a Semiring instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.nonUnitalNonAssocRing {R : Type u_1} {S : Type u_2} [Add S] [Mul S] [Zero S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NonUnitalNonAssocRing R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (neg : ∀ (x : S), f (-x) = -f x) (sub : ∀ (x y : S), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x) : NonUnitalNonAssocRing S

Pullback a NonUnitalNonAssocRing instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.nonUnitalRing {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NonUnitalRing R] (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (neg : ∀ (x : S), f (-x) = -f x) (sub : ∀ (x y : S), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x) : NonUnitalRing S

Pullback a NonUnitalRing instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.nonAssocRing {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NatCast S] [IntCast S] [NonAssocRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (neg : ∀ (x : S), f (-x) = -f x) (sub : ∀ (x y : S), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) : NonAssocRing S

Pullback a NonAssocRing instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.ring {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [Pow S ℕ] [NatCast S] [IntCast S] [Ring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (neg : ∀ (x : S), f (-x) = -f x) (sub : ∀ (x y : S), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x) (npow : ∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) : Ring S

Pullback a Ring instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.nonUnitalNonAssocCommSemiring {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalNonAssocCommSemiring R] (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) : NonUnitalNonAssocCommSemiring S

Pullback a NonUnitalNonAssocCommSemiring instance along an injective function.

Equations

• Function.Injective.nonUnitalNonAssocCommSemiring f hf zero add mul nsmul = { toNonUnitalNonAssocSemiring := Function.Injective.nonUnitalNonAssocSemiring f hf zero add mul nsmul, mul_comm := ⋯ }

@[reducible, inline]

abbrev Function.Injective.nonUnitalCommSemiring {R : Type u_1} {S : Type u_2} [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalCommSemiring R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) : NonUnitalCommSemiring S

Pullback a NonUnitalCommSemiring instance along an injective function.

Equations

• Function.Injective.nonUnitalCommSemiring f hf zero add mul nsmul = { toNonUnitalSemiring := Function.Injective.nonUnitalSemiring f hf zero add mul nsmul, mul_comm := ⋯ }

@[reducible, inline]

abbrev Function.Injective.commSemiring {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [One S] [SMul ℕ S] [Pow S ℕ] [NatCast S] [CommSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (npow : ∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) : CommSemiring S

Pullback a CommSemiring instance along an injective function.

Equations

• Function.Injective.commSemiring f hf zero one add mul nsmul npow natCast = { toSemiring := Function.Injective.semiring f hf zero one add mul nsmul npow natCast, mul_comm := ⋯ }

@[reducible, inline]

abbrev Function.Injective.nonUnitalNonAssocCommRing {R : Type u_1} {S : Type u_2} [Add S] [Mul S] [Zero S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NonUnitalNonAssocCommRing R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (neg : ∀ (x : S), f (-x) = -f x) (sub : ∀ (x y : S), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x) : NonUnitalNonAssocCommRing S

Pullback a NonUnitalNonAssocCommRing instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Injective.nonUnitalCommRing {R : Type u_1} {S : Type u_2} [Add S] [Mul S] [Zero S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NonUnitalCommRing R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (neg : ∀ (x : S), f (-x) = -f x) (sub : ∀ (x y : S), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x) : NonUnitalCommRing S

Pullback a NonUnitalCommRing instance along an injective function.

Equations

• Function.Injective.nonUnitalCommRing f hf zero add mul neg sub nsmul zsmul = { toNonUnitalRing := Function.Injective.nonUnitalRing f hf zero add mul neg sub nsmul zsmul, mul_comm := ⋯ }

@[reducible, inline]

abbrev Function.Injective.commRing {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Injective f) [Add S] [Mul S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [Pow S ℕ] [NatCast S] [IntCast S] [CommRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (neg : ∀ (x : S), f (-x) = -f x) (sub : ∀ (x y : S), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x) (npow : ∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) : CommRing S

Pullback a CommRing instance along an injective function.

Equations

• One or more equations did not get rendered due to their size.

theorem Function.Surjective.leftDistribClass {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Mul R] [Add R] [LeftDistribClass R] (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) : LeftDistribClass S

Pushforward a LeftDistribClass instance along a surjective function.

theorem Function.Surjective.rightDistribClass {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Mul R] [Add R] [RightDistribClass R] (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) : RightDistribClass S

Pushforward a RightDistribClass instance along a surjective function.

@[reducible, inline]

abbrev Function.Surjective.distrib {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Distrib R] (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) : Distrib S

Pushforward a Distrib instance along a surjective function.

Equations

• Function.Surjective.distrib f hf add mul = { toMul := inst✝¹, toAdd := inst✝², left_distrib := ⋯, right_distrib := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.hasDistribNeg {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Mul S] [Neg S] [Mul R] [HasDistribNeg R] (neg : ∀ (a : R), f (-a) = -f a) (mul : ∀ (a b : R), f (a * b) = f a * f b) : HasDistribNeg S

A type endowed with - and * has distributive negation, if it admits a surjective map that preserves - and * from a type which has distributive negation.

Equations

• Function.Surjective.hasDistribNeg f hf neg mul = { toInvolutiveNeg := Function.Surjective.involutiveNeg f hf neg, neg_mul := ⋯, mul_neg := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.nonUnitalNonAssocSemiring {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalNonAssocSemiring R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) : NonUnitalNonAssocSemiring S

Pushforward a NonUnitalNonAssocSemiring instance along a surjective function. See note [reducible non-instances].

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.nonUnitalSemiring {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalSemiring R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) : NonUnitalSemiring S

Pushforward a NonUnitalSemiring instance along a surjective function.

Equations

• Function.Surjective.nonUnitalSemiring f hf zero add mul nsmul = { toNonUnitalNonAssocSemiring := Function.Surjective.nonUnitalNonAssocSemiring f hf zero add mul nsmul, mul_assoc := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.nonAssocSemiring {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [One S] [SMul ℕ S] [NatCast S] [NonAssocSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (natCast : ∀ (n : ℕ), f ↑n = ↑n) : NonAssocSemiring S

Pushforward a NonAssocSemiring instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.semiring {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [One S] [SMul ℕ S] [Pow S ℕ] [NatCast S] [Semiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (npow : ∀ (x : R) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) : Semiring S

Pushforward a Semiring instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.nonUnitalNonAssocRing {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NonUnitalNonAssocRing R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x) : NonUnitalNonAssocRing S

Pushforward a NonUnitalNonAssocRing instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.nonUnitalRing {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NonUnitalRing R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x) : NonUnitalRing S

Pushforward a NonUnitalRing instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.nonAssocRing {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NatCast S] [IntCast S] [NonAssocRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) : NonAssocRing S

Pushforward a NonAssocRing instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.ring {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [Pow S ℕ] [NatCast S] [IntCast S] [Ring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x) (npow : ∀ (x : R) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) : Ring S

Pushforward a Ring instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.nonUnitalNonAssocCommSemiring {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalNonAssocCommSemiring R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) : NonUnitalNonAssocCommSemiring S

Pushforward a NonUnitalNonAssocCommSemiring instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.nonUnitalCommSemiring {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [SMul ℕ S] [NonUnitalCommSemiring R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) : NonUnitalCommSemiring S

Pushforward a NonUnitalCommSemiring instance along a surjective function.

Equations

• Function.Surjective.nonUnitalCommSemiring f hf zero add mul nsmul = { toNonUnitalSemiring := Function.Surjective.nonUnitalSemiring f hf zero add mul nsmul, mul_comm := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.commSemiring {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [One S] [SMul ℕ S] [Pow S ℕ] [NatCast S] [CommSemiring R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (npow : ∀ (x : R) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) : CommSemiring S

Pushforward a CommSemiring instance along a surjective function.

Equations

• Function.Surjective.commSemiring f hf zero one add mul nsmul npow natCast = { toSemiring := Function.Surjective.semiring f hf zero one add mul nsmul npow natCast, mul_comm := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.nonUnitalNonAssocCommRing {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NonUnitalNonAssocCommRing R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x) : NonUnitalNonAssocCommRing S

Pushforward a NonUnitalNonAssocCommRing instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Function.Surjective.nonUnitalCommRing {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NonUnitalCommRing R] (zero : f 0 = 0) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x) : NonUnitalCommRing S

Pushforward a NonUnitalCommRing instance along a surjective function.

Equations

• Function.Surjective.nonUnitalCommRing f hf zero add mul neg sub nsmul zsmul = { toNonUnitalRing := Function.Surjective.nonUnitalRing f hf zero add mul neg sub nsmul zsmul, mul_comm := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.commRing {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Mul S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [Pow S ℕ] [NatCast S] [IntCast S] [CommRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x) (npow : ∀ (x : R) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) : CommRing S

Pushforward a CommRing instance along a surjective function.

Equations

• One or more equations did not get rendered due to their size.

instance AddOpposite.instHasDistribNeg {R : Type u_1} [Mul R] [HasDistribNeg R] : HasDistribNeg Rᵃᵒᵖ

Equations

• AddOpposite.instHasDistribNeg = Function.Injective.hasDistribNeg AddOpposite.unop ⋯ ⋯ ⋯