Pi instances for ring #
This file defines instances for ring, semiring and related structures on Pi Types
Equations
- pi.distrib = {mul := has_mul.mul pi.has_mul, add := has_add.add pi.has_add, left_distrib := _, right_distrib := _}
Equations
- pi.non_unital_non_assoc_semiring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (ᾰ : ℕ) (ᾰ_1 : Π (i : I), f i) (i : I), non_unital_non_assoc_semiring.nsmul ᾰ (ᾰ_1 i), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
Equations
- pi.non_unital_semiring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (ᾰ : ℕ) (ᾰ_1 : Π (i : I), f i) (i : I), non_unital_semiring.nsmul ᾰ (ᾰ_1 i), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
Equations
- pi.non_assoc_semiring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (ᾰ : ℕ) (ᾰ_1 : Π (i : I), f i) (i : I), non_assoc_semiring.nsmul ᾰ (ᾰ_1 i), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := 1, one_mul := _, mul_one := _, nat_cast := λ (ᾰ : ℕ) (i : I), non_assoc_semiring.nat_cast ᾰ, nat_cast_zero := _, nat_cast_succ := _}
Equations
- pi.semiring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := λ (ᾰ : ℕ) (i : I), semiring.nat_cast ᾰ, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _}
Equations
- pi.non_unital_comm_semiring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
Equations
- pi.comm_semiring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := λ (ᾰ : ℕ) (i : I), comm_semiring.nat_cast ᾰ, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
Equations
- pi.non_unital_non_assoc_ring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg pi.has_neg, sub := λ (ᾰ ᾰ_1 : Π (i : I), f i) (i : I), non_unital_non_assoc_ring.sub (ᾰ i) (ᾰ_1 i), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul pi.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
Equations
- pi.non_unital_ring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg pi.has_neg, sub := λ (ᾰ ᾰ_1 : Π (i : I), f i) (i : I), non_unital_ring.sub (ᾰ i) (ᾰ_1 i), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul pi.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
Equations
- pi.non_assoc_ring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg pi.has_neg, sub := λ (ᾰ ᾰ_1 : Π (i : I), f i) (i : I), non_assoc_ring.sub (ᾰ i) (ᾰ_1 i), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul pi.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := λ (i : I), non_assoc_ring.one, one_mul := _, mul_one := _, nat_cast := λ (ᾰ : ℕ) (i : I), non_assoc_ring.nat_cast ᾰ, nat_cast_zero := _, nat_cast_succ := _, int_cast := λ (ᾰ : ℤ) (i : I), non_assoc_ring.int_cast ᾰ, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
Equations
- pi.ring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg pi.has_neg, sub := λ (ᾰ ᾰ_1 : Π (i : I), f i) (i : I), ring.sub (ᾰ i) (ᾰ_1 i), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul pi.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := λ (ᾰ : ℤ) (i : I), ring.int_cast ᾰ, nat_cast := λ (ᾰ : ℕ) (i : I), ring.nat_cast ᾰ, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul pi.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
Equations
- pi.non_unital_comm_ring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg pi.has_neg, sub := λ (ᾰ ᾰ_1 : Π (i : I), f i) (i : I), non_unital_comm_ring.sub (ᾰ i) (ᾰ_1 i), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul pi.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul pi.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}
Equations
- pi.comm_ring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg pi.has_neg, sub := λ (ᾰ ᾰ_1 : Π (i : I), f i) (i : I), comm_ring.sub (ᾰ i) (ᾰ_1 i), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul pi.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := λ (ᾰ : ℤ) (i : I), comm_ring.int_cast ᾰ, nat_cast := λ (ᾰ : ℕ) (i : I), comm_ring.nat_cast ᾰ, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul pi.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
A family of non-unital ring homomorphisms f a : γ →ₙ+* β a
defines a non-unital ring
homomorphism pi.non_unital_ring_hom f : γ →+* Π a, β a
given by
pi.non_unital_ring_hom f x b = f b x
.
A family of ring homomorphisms f a : γ →+* β a
defines a ring homomorphism
pi.ring_hom f : γ →+* Π a, β a
given by pi.ring_hom f x b = f b x
.
Evaluation of functions into an indexed collection of non-unital rings at a point is a
non-unital ring homomorphism. This is function.eval
as a non_unital_ring_hom
.
Equations
- pi.eval_non_unital_ring_hom f i = {to_fun := (pi.eval_mul_hom f i).to_fun, map_mul' := _, map_zero' := _, map_add' := _}
function.const
as a non_unital_ring_hom
.
Equations
- pi.const_non_unital_ring_hom α β = {to_fun := function.const α, map_mul' := _, map_zero' := _, map_add' := _}
Non-unital ring homomorphism between the function spaces I → α
and I → β
, induced by a
non-unital ring homomorphism f
between α
and β
.
Evaluation of functions into an indexed collection of rings at a point is a ring
homomorphism. This is function.eval
as a ring_hom
.
Equations
- pi.eval_ring_hom f i = {to_fun := (pi.eval_monoid_hom f i).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
function.const
as a ring_hom
.
Equations
- pi.const_ring_hom α β = {to_fun := function.const α, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Ring homomorphism between the function spaces I → α
and I → β
, induced by a ring
homomorphism f
between α
and β
.