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

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

Pullback a LeftDistribClass instance along an injective function.

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

Pullback a RightDistribClass instance along an injective function.

@[reducible, inline]

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

Pullback a Distrib instance along an injective function.

Equations

• Function.Injective.distrib f hf add mul = Distrib.mk ⋯ ⋯

@[reducible, inline]

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

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 = HasDistribNeg.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.nonUnitalNonAssocSemiring {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [SMul ℕ β] [NonUnitalNonAssocSemiring α] (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 β

Pullback a NonUnitalNonAssocSemiring instance along an injective function.

Equations

• Function.Injective.nonUnitalNonAssocSemiring f hf zero add mul nsmul = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.nonUnitalSemiring {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [SMul ℕ β] [NonUnitalSemiring α] (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 β

Pullback a NonUnitalSemiring instance along an injective function.

Equations

• Function.Injective.nonUnitalSemiring f hf zero add mul nsmul = NonUnitalSemiring.mk ⋯

@[reducible, inline]

abbrev Function.Injective.nonAssocSemiring {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [One β] [SMul ℕ β] [NatCast β] [NonAssocSemiring α] (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 β

Pullback a NonAssocSemiring instance along an injective function.

Equations

• Function.Injective.nonAssocSemiring f hf zero one add mul nsmul natCast = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.semiring {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [One β] [SMul ℕ β] [Pow β ℕ] [NatCast β] [Semiring α] (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 β

Pullback a Semiring instance along an injective function.

Equations

• Function.Injective.semiring f hf zero one add mul nsmul npow natCast = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.nonUnitalNonAssocRing {α : Type u_1} {β : Type u_2} [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NonUnitalNonAssocRing α] (f : β → α) (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 β

Pullback a NonUnitalNonAssocRing instance along an injective function.

Equations

• Function.Injective.nonUnitalNonAssocRing f hf zero add mul neg sub nsmul zsmul = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.nonUnitalRing {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NonUnitalRing α] (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 β

Pullback a NonUnitalRing instance along an injective function.

Equations

• Function.Injective.nonUnitalRing f hf zero add mul neg sub nsmul zsmul = NonUnitalRing.mk ⋯

@[reducible, inline]

abbrev Function.Injective.nonAssocRing {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NatCast β] [IntCast β] [NonAssocRing α] (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 β

Pullback a NonAssocRing instance along an injective function.

Equations

• Function.Injective.nonAssocRing f hf zero one add mul neg sub nsmul zsmul natCast intCast = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.ring {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] [Ring α] (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 β

Pullback a Ring instance along an injective function.

Equations

• Function.Injective.ring f hf zero one add mul neg sub nsmul zsmul npow natCast intCast = Ring.mk ⋯ AddGroupWithOne.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.nonUnitalNonAssocCommSemiring {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [SMul ℕ β] [NonUnitalNonAssocCommSemiring α] (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 β

Pullback a NonUnitalNonAssocCommSemiring instance along an injective function.

Equations

• Function.Injective.nonUnitalNonAssocCommSemiring f hf zero add mul nsmul = NonUnitalNonAssocCommSemiring.mk ⋯

@[reducible, inline]

abbrev Function.Injective.nonUnitalCommSemiring {α : Type u_1} {β : Type u_2} [Add β] [Mul β] [Zero β] [SMul ℕ β] [NonUnitalCommSemiring α] (f : β → α) (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 β

Pullback a NonUnitalCommSemiring instance along an injective function.

Equations

• Function.Injective.nonUnitalCommSemiring f hf zero add mul nsmul = NonUnitalCommSemiring.mk ⋯

@[reducible, inline]

abbrev Function.Injective.commSemiring {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [One β] [SMul ℕ β] [Pow β ℕ] [NatCast β] [CommSemiring α] (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 β

Pullback a CommSemiring instance along an injective function.

Equations

• Function.Injective.commSemiring f hf zero one add mul nsmul npow natCast = CommSemiring.mk ⋯

@[reducible, inline]

abbrev Function.Injective.nonUnitalNonAssocCommRing {α : Type u_1} {β : Type u_2} [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NonUnitalNonAssocCommRing α] (f : β → α) (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 β

Pullback a NonUnitalNonAssocCommRing instance along an injective function.

Equations

• Function.Injective.nonUnitalNonAssocCommRing f hf zero add mul neg sub nsmul zsmul = NonUnitalNonAssocCommRing.mk ⋯

@[reducible, inline]

abbrev Function.Injective.nonUnitalCommRing {α : Type u_1} {β : Type u_2} [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NonUnitalCommRing α] (f : β → α) (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 β

Pullback a NonUnitalCommRing instance along an injective function.

Equations

• Function.Injective.nonUnitalCommRing f hf zero add mul neg sub nsmul zsmul = NonUnitalCommRing.mk ⋯

@[reducible, inline]

abbrev Function.Injective.commRing {α : Type u_1} {β : Type u_2} (f : β → α) (hf : Injective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] [CommRing α] (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 β

Pullback a CommRing instance along an injective function.

Equations

• Function.Injective.commRing f hf zero one add mul neg sub nsmul zsmul npow natCast intCast = CommRing.mk ⋯

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

Pushforward a LeftDistribClass instance along a surjective function.

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

Pushforward a RightDistribClass instance along a surjective function.

@[reducible, inline]

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

Pushforward a Distrib instance along a surjective function.

Equations

• Function.Surjective.distrib f hf add mul = Distrib.mk ⋯ ⋯

@[reducible, inline]

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

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 = HasDistribNeg.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.nonUnitalNonAssocSemiring {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [SMul ℕ β] [NonUnitalNonAssocSemiring α] (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 β

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

Equations

• Function.Surjective.nonUnitalNonAssocSemiring f hf zero add mul nsmul = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.nonUnitalSemiring {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [SMul ℕ β] [NonUnitalSemiring α] (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 β

Pushforward a NonUnitalSemiring instance along a surjective function.

Equations

• Function.Surjective.nonUnitalSemiring f hf zero add mul nsmul = NonUnitalSemiring.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.nonAssocSemiring {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [One β] [SMul ℕ β] [NatCast β] [NonAssocSemiring α] (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 β

Pushforward a NonAssocSemiring instance along a surjective function.

Equations

• Function.Surjective.nonAssocSemiring f hf zero one add mul nsmul natCast = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.semiring {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [One β] [SMul ℕ β] [Pow β ℕ] [NatCast β] [Semiring α] (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 β

Pushforward a Semiring instance along a surjective function.

Equations

• Function.Surjective.semiring f hf zero one add mul nsmul npow natCast = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.nonUnitalNonAssocRing {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NonUnitalNonAssocRing α] (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 β

Pushforward a NonUnitalNonAssocRing instance along a surjective function.

Equations

• Function.Surjective.nonUnitalNonAssocRing f hf zero add mul neg sub nsmul zsmul = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.nonUnitalRing {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NonUnitalRing α] (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 β

Pushforward a NonUnitalRing instance along a surjective function.

Equations

• Function.Surjective.nonUnitalRing f hf zero add mul neg sub nsmul zsmul = NonUnitalRing.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.nonAssocRing {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NatCast β] [IntCast β] [NonAssocRing α] (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 β

Pushforward a NonAssocRing instance along a surjective function.

Equations

• Function.Surjective.nonAssocRing f hf zero one add mul neg sub nsmul zsmul natCast intCast = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.ring {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] [Ring α] (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 β

Pushforward a Ring instance along a surjective function.

Equations

• Function.Surjective.ring f hf zero one add mul neg sub nsmul zsmul npow natCast intCast = Ring.mk ⋯ AddGroupWithOne.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.nonUnitalNonAssocCommSemiring {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [SMul ℕ β] [NonUnitalNonAssocCommSemiring α] (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 β

Pushforward a NonUnitalNonAssocCommSemiring instance along a surjective function.

Equations

• Function.Surjective.nonUnitalNonAssocCommSemiring f hf zero add mul nsmul = NonUnitalNonAssocCommSemiring.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.nonUnitalCommSemiring {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [SMul ℕ β] [NonUnitalCommSemiring α] (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 β

Pushforward a NonUnitalCommSemiring instance along a surjective function.

Equations

• Function.Surjective.nonUnitalCommSemiring f hf zero add mul nsmul = NonUnitalCommSemiring.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.commSemiring {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [One β] [SMul ℕ β] [Pow β ℕ] [NatCast β] [CommSemiring α] (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 β

Pushforward a CommSemiring instance along a surjective function.

Equations

• Function.Surjective.commSemiring f hf zero one add mul nsmul npow natCast = CommSemiring.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.nonUnitalNonAssocCommRing {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NonUnitalNonAssocCommRing α] (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 β

Pushforward a NonUnitalNonAssocCommRing instance along a surjective function.

Equations

• Function.Surjective.nonUnitalNonAssocCommRing f hf zero add mul neg sub nsmul zsmul = NonUnitalNonAssocCommRing.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.nonUnitalCommRing {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [NonUnitalCommRing α] (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 β

Pushforward a NonUnitalCommRing instance along a surjective function.

Equations

• Function.Surjective.nonUnitalCommRing f hf zero add mul neg sub nsmul zsmul = NonUnitalCommRing.mk ⋯

@[reducible, inline]

abbrev Function.Surjective.commRing {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Surjective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] [CommRing α] (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 β

Pushforward a CommRing instance along a surjective function.

Equations

• Function.Surjective.commRing f hf zero one add mul neg sub nsmul zsmul npow natCast intCast = CommRing.mk ⋯

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

Equations

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