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

Distrib class

ink

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

Pullback a Distrib instance along an injective function. See note [reducible non-instances].

Equations

• Function.Injective.distrib f hf add mul = Distrib.mk (_ : ∀ (x y z : R), x * (y + z) = x * y + x * z) (_ : ∀ (x y z : R), (x + y) * z = x * z + y * z)

ink

def Function.Surjective.distrib {R : Type x} {S : Type u_1} [inst : Distrib R] [inst : Add S] [inst : Mul S] (f : R → S) (hf : Function.Surjective f) (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. See note [reducible non-instances].

Equations

• Function.Surjective.distrib f hf add mul = Distrib.mk (_ : ∀ (y₁ y₂ y₃ : S), y₁ * (y₂ + y₃) = y₁ * y₂ + y₁ * y₃) (_ : ∀ (y₁ y₂ y₃ : S), (y₁ + y₂) * y₃ = y₁ * y₃ + y₂ * y₃)

Semirings

ink

def Function.Injective.nonUnitalNonAssocSemiring {β : Type v} [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : SMul ℕ β] {α : Type u} [inst : NonUnitalNonAssocSemiring α] (f : β → α) (hf : Function.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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) : NonUnitalNonAssocSemiring β

Pullback a NonUnitalNonAssocRing instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.nonUnitalSemiring {β : Type v} [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : SMul ℕ β] {α : Type u} [inst : NonUnitalSemiring α] (f : β → α) (hf : Function.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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) : NonUnitalSemiring β

Pullback a NonUnitalSemiring instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.nonAssocSemiring {α : Type u} [inst : NonAssocSemiring α] {β : Type v} [inst : Zero β] [inst : One β] [inst : Mul β] [inst : Add β] [inst : SMul ℕ β] [inst : NatCast β] (f : β → α) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : NonAssocSemiring β

Pullback a NonAssocSemiring instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.semiring {α : Type u} [inst : Semiring α] {β : Type v} [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Pow β ℕ] [inst : SMul ℕ β] [inst : NatCast β] (f : β → α) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : Semiring β

Pullback a Semiring instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.nonUnitalNonAssocSemiring {β : Type v} [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : SMul ℕ β] {α : Type u} [inst : NonUnitalNonAssocSemiring α] (f : α → β) (hf : Function.Surjective 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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) : NonUnitalNonAssocSemiring β

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.

ink

def Function.Surjective.nonUnitalSemiring {β : Type v} [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : SMul ℕ β] {α : Type u} [inst : NonUnitalSemiring α] (f : α → β) (hf : Function.Surjective 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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) : NonUnitalSemiring β

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

Equations

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

ink

def Function.Surjective.nonAssocSemiring {α : Type u} [inst : NonAssocSemiring α] {β : Type v} [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : SMul ℕ β] [inst : NatCast β] (f : α → β) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : NonAssocSemiring β

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

Equations

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

ink

def Function.Surjective.semiring {α : Type u} [inst : Semiring α] {β : Type v} [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Pow β ℕ] [inst : SMul ℕ β] [inst : NatCast β] (f : α → β) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : Semiring β

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

Equations

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

ink

def Function.Injective.nonUnitalCommSemiring {α : Type u} {γ : Type w} [inst : NonUnitalCommSemiring α] [inst : Zero γ] [inst : Add γ] [inst : Mul γ] [inst : SMul ℕ γ] (f : γ → α) (hf : Function.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 : ∀ (x : γ) (n : ℕ), f (n • x) = n • f x) : NonUnitalCommSemiring γ

Pullback a NonUnitalCommSemiring instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.nonUnitalCommSemiring {α : Type u} {γ : Type w} [inst : NonUnitalCommSemiring α] [inst : Zero γ] [inst : Add γ] [inst : Mul γ] [inst : SMul ℕ γ] (f : α → γ) (hf : Function.Surjective 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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) : NonUnitalCommSemiring γ

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

Equations

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

ink

def Function.Injective.commSemiring {α : Type u} {γ : Type w} [inst : CommSemiring α] [inst : Zero γ] [inst : One γ] [inst : Add γ] [inst : Mul γ] [inst : SMul ℕ γ] [inst : NatCast γ] [inst : Pow γ ℕ] (f : γ → α) (hf : Function.Injective f) (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 : ∀ (x : γ) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : γ) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : CommSemiring γ

Pullback a CommSemiring instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.commSemiring {α : Type u} {γ : Type w} [inst : CommSemiring α] [inst : Zero γ] [inst : One γ] [inst : Add γ] [inst : Mul γ] [inst : SMul ℕ γ] [inst : NatCast γ] [inst : Pow γ ℕ] (f : α → γ) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : CommSemiring γ

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

Equations

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

ink

def Function.Injective.hasDistribNeg {α : Type u} {β : Type v} [inst : Mul α] [inst : HasDistribNeg α] [inst : Neg β] [inst : Mul β] (f : β → α) (hf : Function.Injective f) (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

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

ink

def Function.Surjective.hasDistribNeg {α : Type u} {β : Type v} [inst : Mul α] [inst : HasDistribNeg α] [inst : Neg β] [inst : Mul β] (f : α → β) (hf : Function.Surjective f) (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

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

ink

instance AddOpposite.instHasDistribNegAddOppositeInstMulAddOpposite {α : Type u} [inst : Mul α] [inst : HasDistribNeg α] : HasDistribNeg αᵃᵒᵖ

Equations

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

Rings

ink

def Function.Injective.nonUnitalNonAssocRing {α : Type u} {β : Type v} [inst : NonUnitalNonAssocRing α] [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] (f : β → α) (hf : Function.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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) : NonUnitalNonAssocRing β

Pullback a NonUnitalNonAssocRing instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.nonUnitalNonAssocRing {α : Type u} {β : Type v} [inst : NonUnitalNonAssocRing α] [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] (f : α → β) (hf : Function.Surjective 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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) : NonUnitalNonAssocRing β

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

Equations

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

ink

def Function.Injective.nonUnitalRing {α : Type u} {β : Type v} [inst : NonUnitalRing α] [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] (f : β → α) (hf : Function.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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (gsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) : NonUnitalRing β

Pullback a NonUnitalRing instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.nonUnitalRing {α : Type u} {β : Type v} [inst : NonUnitalRing α] [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] (f : α → β) (hf : Function.Surjective 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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (gsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) : NonUnitalRing β

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

Equations

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

ink

def Function.Injective.nonAssocRing {α : Type u} {β : Type v} [inst : NonAssocRing α] [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] [inst : NatCast β] [inst : IntCast β] (f : β → α) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (gsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : NonAssocRing β

Pullback a NonAssocRing instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.nonAssocRing {α : Type u} {β : Type v} [inst : NonAssocRing α] [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] [inst : NatCast β] [inst : IntCast β] (f : α → β) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (gsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : NonAssocRing β

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

Equations

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

ink

def Function.Injective.ring {α : Type u} {β : Type v} [inst : Ring α] [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] [inst : Pow β ℕ] [inst : NatCast β] [inst : IntCast β] (f : β → α) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : Ring β

Pullback a Ring instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.ring {α : Type u} {β : Type v} [inst : Ring α] [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] [inst : Pow β ℕ] [inst : NatCast β] [inst : IntCast β] (f : α → β) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : Ring β

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

Equations

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

ink

def Function.Injective.nonUnitalCommRing {α : Type u} {β : Type v} [inst : NonUnitalCommRing α] [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] (f : β → α) (hf : Function.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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) : NonUnitalCommRing β

Pullback a NonUnitalCommRing instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.nonUnitalCommRing {α : Type u} {β : Type v} [inst : NonUnitalCommRing α] [inst : Zero β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] (f : α → β) (hf : Function.Surjective 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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) : NonUnitalCommRing β

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

Equations

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

ink

def Function.Injective.commRing {α : Type u} {β : Type v} [inst : CommRing α] [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] [inst : Pow β ℕ] [inst : NatCast β] [inst : IntCast β] (f : β → α) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : CommRing β

Pullback a CommRing instance along an injective function. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.commRing {α : Type u} {β : Type v} [inst : CommRing α] [inst : Zero β] [inst : One β] [inst : Add β] [inst : Mul β] [inst : Neg β] [inst : Sub β] [inst : SMul ℕ β] [inst : SMul ℤ β] [inst : Pow β ℕ] [inst : NatCast β] [inst : IntCast β] (f : α → β) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : α) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x : α) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : CommRing β

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

Equations

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