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

Implementation note

The nsmul and zsmul assumptions on any transfer definition for an algebraic structure involving both addition and multiplication (eg AddMonoidWithOne) is ∀ n x, f (n • x) = n • f x, which is what we would expect. However, we cannot do the same for transfer definitions built using to_additive (eg AddMonoid) as we want the multiplicative versions to be ∀ x n, f (x ^ n) = f x ^ n. As a result, we must use Function.swap when using additivised transfer definitions in non-additivised ones.

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.addMonoidWithOne {R : Type u_1} {S : Type u_2} [Zero S] [One S] [Add S] [SMul ℕ S] [NatCast S] [AddMonoidWithOne R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (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) : AddMonoidWithOne S

A type endowed with 0, 1 and + is an additive monoid with one, if it admits an injective map that preserves 0, 1 and + to an additive monoid with one. See note [reducible non-instances].

Equations

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

@[reducible, inline]

abbrev Function.Injective.addCommMonoidWithOne {R : Type u_1} {S : Type u_3} [Zero S] [One S] [Add S] [SMul ℕ S] [NatCast S] [AddCommMonoidWithOne R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (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) : AddCommMonoidWithOne S

A type endowed with 0, 1 and + is an additive commutative monoid with one, if it admits an injective map that preserves 0, 1 and + to an additive commutative monoid with one. See note [reducible non-instances].

Equations

• Function.Injective.addCommMonoidWithOne f hf zero one add nsmul natCast = { toAddMonoidWithOne := Function.Injective.addMonoidWithOne f hf zero one add nsmul natCast, add_comm := ⋯ }

@[reducible, inline]

abbrev Function.Injective.addGroupWithOne {R : Type u_1} {S : Type u_3} [Zero S] [One S] [Add S] [SMul ℕ S] [Neg S] [Sub S] [SMul ℤ S] [NatCast S] [IntCast S] [AddGroupWithOne R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (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) : AddGroupWithOne S

A type endowed with 0, 1 and + is an additive group with one, if it admits an injective map that preserves 0, 1 and + to an additive group with one. See note [reducible non-instances].

Equations

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

@[reducible, inline]

abbrev Function.Injective.addCommGroupWithOne {R : Type u_1} {S : Type u_3} [Zero S] [One S] [Add S] [SMul ℕ S] [Neg S] [Sub S] [SMul ℤ S] [NatCast S] [IntCast S] [AddCommGroupWithOne R] (f : S → R) (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (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) : AddCommGroupWithOne S

A type endowed with 0, 1 and + is an additive commutative group with one, if it admits an injective map that preserves 0, 1 and + to an additive commutative group with one. See note [reducible non-instances].

Equations

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

@[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.addMonoidWithOne {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Zero S] [One S] [SMul ℕ S] [NatCast S] [AddMonoidWithOne R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (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) : AddMonoidWithOne S

A type endowed with 0, 1 and + is an additive monoid with one, if it admits a surjective map that preserves 0, 1 and * from an additive monoid with one. See note [reducible non-instances].

Equations

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

@[reducible, inline]

abbrev Function.Surjective.addCommMonoidWithOne {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Zero S] [One S] [SMul ℕ S] [NatCast S] [AddCommMonoidWithOne R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (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) : AddCommMonoidWithOne S

A type endowed with 0, 1 and + is an additive monoid with one, if it admits a surjective map that preserves 0, 1 and * from an additive monoid with one. See note [reducible non-instances].

Equations

• Function.Surjective.addCommMonoidWithOne f hf zero one add nsmul natCast = { toAddMonoidWithOne := Function.Surjective.addMonoidWithOne f hf zero one add nsmul natCast, add_comm := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.addGroupWithOne {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NatCast S] [IntCast S] [AddGroupWithOne R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (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) : AddGroupWithOne S

A type endowed with 0, 1, + is an additive group with one, if it admits a surjective map that preserves 0, 1, and + to an additive group with one. See note [reducible non-instances].

Equations

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

@[reducible, inline]

abbrev Function.Surjective.addCommGroupWithOne {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Surjective f) [Add S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NatCast S] [IntCast S] [AddCommGroupWithOne R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (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) : AddCommGroupWithOne S

A type endowed with 0, 1, + is an additive commutative group with one, if it admits a surjective map that preserves 0, 1, and + to an additive commutative group with one. See note [reducible non-instances].

Equations

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

@[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 ⋯ ⋯ ⋯