Pulling back rings along injective maps, and pushing them forward along surjective maps. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, reducible]
def
function.injective.distrib
{R : Type x}
{S : Type u_1}
[has_mul R]
[has_add R]
[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 = {mul := has_mul.mul _inst_1, add := has_add.add _inst_2, left_distrib := _, right_distrib := _}
@[protected, reducible]
def
function.surjective.distrib
{R : Type x}
{S : Type u_1}
[distrib R]
[has_add S]
[has_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 = {mul := has_mul.mul _inst_3, add := has_add.add _inst_2, left_distrib := _, right_distrib := _}
Semirings #
@[protected, reducible]
def
function.injective.non_unital_non_assoc_semiring
{β : Type v}
[has_zero β]
[has_add β]
[has_mul β]
[has_smul ℕ β]
{α : Type u}
[non_unital_non_assoc_semiring α]
(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) :
Pullback a non_unital_non_assoc_semiring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.non_unital_non_assoc_semiring f hf zero add mul nsmul = {add := add_comm_monoid.add (function.injective.add_comm_monoid f hf zero add nsmul), add_assoc := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.injective.add_comm_monoid f hf zero add nsmul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_zero_class.mul (function.injective.mul_zero_class f hf zero mul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.injective.non_unital_semiring
{β : Type v}
[has_zero β]
[has_add β]
[has_mul β]
[has_smul ℕ β]
{α : Type u}
[non_unital_semiring α]
(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) :
Pullback a non_unital_semiring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.non_unital_semiring f hf zero add mul nsmul = {add := non_unital_non_assoc_semiring.add (function.injective.non_unital_non_assoc_semiring f hf zero add mul nsmul), add_assoc := _, zero := non_unital_non_assoc_semiring.zero (function.injective.non_unital_non_assoc_semiring f hf zero add mul nsmul), zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul (function.injective.non_unital_non_assoc_semiring f hf zero add mul nsmul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul (function.injective.non_unital_non_assoc_semiring f hf zero add mul nsmul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, reducible]
def
function.injective.non_assoc_semiring
{α : Type u}
[non_assoc_semiring α]
{β : Type v}
[has_zero β]
[has_one β]
[has_mul β]
[has_add β]
[has_smul ℕ β]
[has_nat_cast β]
(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) :
Pullback a non_assoc_semiring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.non_assoc_semiring f hf zero one add mul nsmul nat_cast = {add := add_monoid_with_one.add (function.injective.add_monoid_with_one f hf zero one add nsmul nat_cast), add_assoc := _, zero := add_monoid_with_one.zero (function.injective.add_monoid_with_one f hf zero one add nsmul nat_cast), zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul (function.injective.add_monoid_with_one f hf zero one add nsmul nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul (function.injective.non_unital_non_assoc_semiring f hf zero add mul nsmul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := add_monoid_with_one.one (function.injective.add_monoid_with_one f hf zero one add nsmul nat_cast), one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast (function.injective.add_monoid_with_one f hf zero one add nsmul nat_cast), nat_cast_zero := _, nat_cast_succ := _}
@[protected, reducible]
def
function.injective.semiring
{α : Type u}
[semiring α]
{β : Type v}
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[has_nat_cast β]
(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
- function.injective.semiring f hf zero one add mul nsmul npow nat_cast = {add := non_assoc_semiring.add (function.injective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), add_assoc := _, zero := non_assoc_semiring.zero (function.injective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul (function.injective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_assoc_semiring.mul (function.injective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := non_assoc_semiring.one (function.injective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast (function.injective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := monoid_with_zero.npow (function.injective.monoid_with_zero f hf zero one mul npow), npow_zero' := _, npow_succ' := _}
@[protected, reducible]
def
function.surjective.non_unital_non_assoc_semiring
{β : Type v}
[has_zero β]
[has_add β]
[has_mul β]
[has_smul ℕ β]
{α : Type u}
[non_unital_non_assoc_semiring α]
(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) :
Pushforward a non_unital_non_assoc_semiring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.non_unital_non_assoc_semiring f hf zero add mul nsmul = {add := add_comm_monoid.add (function.surjective.add_comm_monoid f hf zero add nsmul), add_assoc := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.surjective.add_comm_monoid f hf zero add nsmul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_zero_class.mul (function.surjective.mul_zero_class f hf zero mul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.surjective.non_unital_semiring
{β : Type v}
[has_zero β]
[has_add β]
[has_mul β]
[has_smul ℕ β]
{α : Type u}
[non_unital_semiring α]
(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) :
Pushforward a non_unital_semiring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.non_unital_semiring f hf zero add mul nsmul = {add := non_unital_non_assoc_semiring.add (function.surjective.non_unital_non_assoc_semiring f hf zero add mul nsmul), add_assoc := _, zero := non_unital_non_assoc_semiring.zero (function.surjective.non_unital_non_assoc_semiring f hf zero add mul nsmul), zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul (function.surjective.non_unital_non_assoc_semiring f hf zero add mul nsmul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul (function.surjective.non_unital_non_assoc_semiring f hf zero add mul nsmul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, reducible]
def
function.surjective.non_assoc_semiring
{α : Type u}
[non_assoc_semiring α]
{β : Type v}
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_smul ℕ β]
[has_nat_cast β]
(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) :
Pushforward a non_assoc_semiring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.non_assoc_semiring f hf zero one add mul nsmul nat_cast = {add := add_monoid_with_one.add (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), add_assoc := _, zero := add_monoid_with_one.zero (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul (function.surjective.non_unital_non_assoc_semiring f hf zero add mul nsmul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := add_monoid_with_one.one (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), nat_cast_zero := _, nat_cast_succ := _}
@[protected, reducible]
def
function.surjective.semiring
{α : Type u}
[semiring α]
{β : Type v}
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[has_nat_cast β]
(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
- function.surjective.semiring f hf zero one add mul nsmul npow nat_cast = {add := non_assoc_semiring.add (function.surjective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), add_assoc := _, zero := non_assoc_semiring.zero (function.surjective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul (function.surjective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_assoc_semiring.mul (function.surjective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := non_assoc_semiring.one (function.surjective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast (function.surjective.non_assoc_semiring f hf zero one add mul nsmul nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := monoid_with_zero.npow (function.surjective.monoid_with_zero f hf zero one mul npow), npow_zero' := _, npow_succ' := _}
@[protected, reducible]
def
function.injective.non_unital_comm_semiring
{α : Type u}
{γ : Type w}
[non_unital_comm_semiring α]
[has_zero γ]
[has_add γ]
[has_mul γ]
[has_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) :
Pullback a non_unital_semiring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.non_unital_comm_semiring f hf zero add mul nsmul = {add := non_unital_semiring.add (function.injective.non_unital_semiring f hf zero add mul nsmul), add_assoc := _, zero := non_unital_semiring.zero (function.injective.non_unital_semiring f hf zero add mul nsmul), zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul (function.injective.non_unital_semiring f hf zero add mul nsmul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_semiring.mul (function.injective.non_unital_semiring f hf zero add mul nsmul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
@[protected, reducible]
def
function.surjective.non_unital_comm_semiring
{α : Type u}
{γ : Type w}
[non_unital_comm_semiring α]
[has_zero γ]
[has_add γ]
[has_mul γ]
[has_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) :
Pushforward a non_unital_semiring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.non_unital_comm_semiring f hf zero add mul nsmul = {add := non_unital_semiring.add (function.surjective.non_unital_semiring f hf zero add mul nsmul), add_assoc := _, zero := non_unital_semiring.zero (function.surjective.non_unital_semiring f hf zero add mul nsmul), zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul (function.surjective.non_unital_semiring f hf zero add mul nsmul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_semiring.mul (function.surjective.non_unital_semiring f hf zero add mul nsmul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
@[protected, reducible]
def
function.injective.comm_semiring
{α : Type u}
{γ : Type w}
[comm_semiring α]
[has_zero γ]
[has_one γ]
[has_add γ]
[has_mul γ]
[has_smul ℕ γ]
[has_nat_cast γ]
[has_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) :
Pullback a semiring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast = {add := semiring.add (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := semiring.zero (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := semiring.nsmul (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, reducible]
def
function.surjective.comm_semiring
{α : Type u}
{γ : Type w}
[comm_semiring α]
[has_zero γ]
[has_one γ]
[has_add γ]
[has_mul γ]
[has_smul ℕ γ]
[has_nat_cast γ]
[has_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) :
Pushforward a semiring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.comm_semiring f hf zero one add mul nsmul npow nat_cast = {add := semiring.add (function.surjective.semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := semiring.zero (function.surjective.semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := semiring.nsmul (function.surjective.semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (function.surjective.semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (function.surjective.semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (function.surjective.semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (function.surjective.semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, reducible]
def
function.injective.has_distrib_neg
{α : Type u}
{β : Type v}
[has_mul α]
[has_distrib_neg α]
[has_neg β]
[has_mul β]
(f : β → α)
(hf : function.injective f)
(neg : ∀ (a : β), f (-a) = -f a)
(mul : ∀ (a b : β), f (a * b) = f a * f b) :
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.has_distrib_neg f hf neg mul = {neg := has_involutive_neg.neg (function.injective.has_involutive_neg f hf neg), neg_neg := _, neg_mul := _, mul_neg := _}
@[protected, reducible]
def
function.surjective.has_distrib_neg
{α : Type u}
{β : Type v}
[has_mul α]
[has_distrib_neg α]
[has_neg β]
[has_mul β]
(f : α → β)
(hf : function.surjective f)
(neg : ∀ (a : α), f (-a) = -f a)
(mul : ∀ (a b : α), f (a * b) = f a * f b) :
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.has_distrib_neg f hf neg mul = {neg := has_involutive_neg.neg (function.surjective.has_involutive_neg f hf neg), neg_neg := _, neg_mul := _, mul_neg := _}
@[protected, instance]
Equations
- add_opposite.has_distrib_neg = function.injective.has_distrib_neg add_opposite.unop add_opposite.unop_injective add_opposite.has_distrib_neg._proof_1 add_opposite.unop_mul
Rings #
@[protected, reducible]
def
function.injective.non_unital_non_assoc_ring
{α : Type u}
{β : Type v}
[non_unital_non_assoc_ring α]
[has_zero β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_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) :
Pullback a non_unital_non_assoc_ring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.non_unital_non_assoc_ring f hf zero add mul neg sub nsmul zsmul = {add := add_comm_group.add (function.injective.add_comm_group f hf zero add neg sub nsmul zsmul), add_assoc := _, zero := add_comm_group.zero (function.injective.add_comm_group f hf zero add neg sub nsmul zsmul), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (function.injective.add_comm_group f hf zero add neg sub nsmul zsmul), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.injective.add_comm_group f hf zero add neg sub nsmul zsmul), sub := add_comm_group.sub (function.injective.add_comm_group f hf zero add neg sub nsmul zsmul), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (function.injective.add_comm_group f hf zero add neg sub nsmul zsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul_zero_class.mul (function.injective.mul_zero_class f hf zero mul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.surjective.non_unital_non_assoc_ring
{α : Type u}
{β : Type v}
[non_unital_non_assoc_ring α]
[has_zero β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_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) :
Pushforward a non_unital_non_assoc_ring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.non_unital_non_assoc_ring f hf zero add mul neg sub nsmul zsmul = {add := add_comm_group.add (function.surjective.add_comm_group f hf zero add neg sub nsmul zsmul), add_assoc := _, zero := add_comm_group.zero (function.surjective.add_comm_group f hf zero add neg sub nsmul zsmul), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (function.surjective.add_comm_group f hf zero add neg sub nsmul zsmul), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.surjective.add_comm_group f hf zero add neg sub nsmul zsmul), sub := add_comm_group.sub (function.surjective.add_comm_group f hf zero add neg sub nsmul zsmul), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (function.surjective.add_comm_group f hf zero add neg sub nsmul zsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul_zero_class.mul (function.surjective.mul_zero_class f hf zero mul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.injective.non_unital_ring
{α : Type u}
{β : Type v}
[non_unital_ring α]
[has_zero β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_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) :
Pullback a non_unital_ring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.non_unital_ring f hf zero add mul neg sub nsmul gsmul = {add := add_comm_group.add (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), add_assoc := _, zero := add_comm_group.zero (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), sub := add_comm_group.sub (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul_zero_class.mul (function.injective.mul_zero_class f hf zero mul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, reducible]
def
function.surjective.non_unital_ring
{α : Type u}
{β : Type v}
[non_unital_ring α]
[has_zero β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_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) :
Pushforward a non_unital_ring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.non_unital_ring f hf zero add mul neg sub nsmul gsmul = {add := add_comm_group.add (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), add_assoc := _, zero := add_comm_group.zero (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), sub := add_comm_group.sub (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul_zero_class.mul (function.surjective.mul_zero_class f hf zero mul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, reducible]
def
function.injective.non_assoc_ring
{α : Type u}
{β : Type v}
[non_assoc_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_nat_cast β]
[has_int_cast β]
(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) :
Pullback a non_assoc_ring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.non_assoc_ring f hf zero one add mul neg sub nsmul gsmul nat_cast int_cast = {add := add_comm_group.add (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), add_assoc := _, zero := add_comm_group.zero (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), sub := add_comm_group.sub (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (function.injective.add_comm_group f hf zero add neg sub nsmul gsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul_zero_class.mul (function.injective.mul_zero_class f hf zero mul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := add_group_with_one.one (function.injective.add_group_with_one f hf zero one add neg sub nsmul gsmul nat_cast int_cast), one_mul := _, mul_one := _, nat_cast := add_group_with_one.nat_cast (function.injective.add_group_with_one f hf zero one add neg sub nsmul gsmul nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast := add_group_with_one.int_cast (function.injective.add_group_with_one f hf zero one add neg sub nsmul gsmul nat_cast int_cast), int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[protected, reducible]
def
function.surjective.non_assoc_ring
{α : Type u}
{β : Type v}
[non_assoc_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_nat_cast β]
[has_int_cast β]
(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) :
Pushforward a non_unital_ring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.non_assoc_ring f hf zero one add mul neg sub nsmul gsmul nat_cast int_cast = {add := add_comm_group.add (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), add_assoc := _, zero := add_comm_group.zero (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), sub := add_comm_group.sub (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (function.surjective.add_comm_group f hf zero add neg sub nsmul gsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul_zero_class.mul (function.surjective.mul_zero_class f hf zero mul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := add_group_with_one.one (function.surjective.add_group_with_one f hf zero one add neg sub nsmul gsmul nat_cast int_cast), one_mul := _, mul_one := _, nat_cast := add_group_with_one.nat_cast (function.surjective.add_group_with_one f hf zero one add neg sub nsmul gsmul nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast := add_group_with_one.int_cast (function.surjective.add_group_with_one f hf zero one add neg sub nsmul gsmul nat_cast int_cast), int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[protected, reducible]
def
function.injective.ring
{α : Type u}
{β : Type v}
[ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_pow β ℕ]
[has_nat_cast β]
[has_int_cast β]
(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
- function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast = {add := add_group_with_one.add (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), add_assoc := _, zero := add_group_with_one.zero (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), sub := add_group_with_one.sub (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), nat_cast := add_group_with_one.nat_cast (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), one := add_group_with_one.one (function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := monoid.mul (function.injective.monoid f hf one mul npow), mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow (function.injective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, reducible]
def
function.surjective.ring
{α : Type u}
{β : Type v}
[ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_pow β ℕ]
[has_nat_cast β]
[has_int_cast β]
(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
- function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast = {add := add_group_with_one.add (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), add_assoc := _, zero := add_group_with_one.zero (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), sub := add_group_with_one.sub (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), nat_cast := add_group_with_one.nat_cast (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), one := add_group_with_one.one (function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := monoid.mul (function.surjective.monoid f hf one mul npow), mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow (function.surjective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, reducible]
def
function.injective.non_unital_comm_ring
{α : Type u}
{β : Type v}
[non_unital_comm_ring α]
[has_zero β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_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) :
Pullback a comm_ring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.non_unital_comm_ring f hf zero add mul neg sub nsmul zsmul = {add := non_unital_ring.add (function.injective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), add_assoc := _, zero := non_unital_ring.zero (function.injective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), zero_add := _, add_zero := _, nsmul := non_unital_ring.nsmul (function.injective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_ring.neg (function.injective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), sub := non_unital_ring.sub (function.injective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), sub_eq_add_neg := _, zsmul := non_unital_ring.zsmul (function.injective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_ring.mul (function.injective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
@[protected, reducible]
def
function.surjective.non_unital_comm_ring
{α : Type u}
{β : Type v}
[non_unital_comm_ring α]
[has_zero β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_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) :
Pushforward a non_unital_comm_ring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.non_unital_comm_ring f hf zero add mul neg sub nsmul zsmul = {add := non_unital_ring.add (function.surjective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), add_assoc := _, zero := non_unital_ring.zero (function.surjective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), zero_add := _, add_zero := _, nsmul := non_unital_ring.nsmul (function.surjective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_ring.neg (function.surjective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), sub := non_unital_ring.sub (function.surjective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), sub_eq_add_neg := _, zsmul := non_unital_ring.zsmul (function.surjective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_ring.mul (function.surjective.non_unital_ring f hf zero add mul neg sub nsmul zsmul), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
@[protected, reducible]
def
function.injective.comm_ring
{α : Type u}
{β : Type v}
[comm_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_pow β ℕ]
[has_nat_cast β]
[has_int_cast β]
(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) :
Pullback a comm_ring instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast = {add := ring.add (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), add_assoc := _, zero := ring.zero (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zero_add := _, add_zero := _, nsmul := ring.nsmul (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := ring.sub (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := ring.zsmul (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := ring.nat_cast (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), one := ring.one (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[protected, reducible]
def
function.surjective.comm_ring
{α : Type u}
{β : Type v}
[comm_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_pow β ℕ]
[has_nat_cast β]
[has_int_cast β]
(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) :
Pushforward a comm_ring instance along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast = {add := ring.add (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), add_assoc := _, zero := ring.zero (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zero_add := _, add_zero := _, nsmul := ring.nsmul (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := ring.sub (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := ring.zsmul (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := ring.nat_cast (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), one := ring.one (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (function.surjective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}