Pi instances for groups and monoids #
This file defines instances for group, monoid, semigroup and related structures on Pi types.
Equations
- pi.add_semigroup = {add := has_add.add pi.has_add, add_assoc := _}
Equations
- pi.semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _}
Equations
- pi.semigroup_with_zero = {mul := has_mul.mul pi.has_mul, mul_assoc := _, zero := 0, zero_mul := _, mul_zero := _}
Equations
- pi.comm_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_comm := _}
Equations
- pi.add_comm_semigroup = {add := has_add.add pi.has_add, add_assoc := _, add_comm := _}
Equations
- pi.mul_one_class = {one := 1, mul := has_mul.mul pi.has_mul, one_mul := _, mul_one := _}
Equations
- pi.add_zero_class = {zero := 0, add := has_add.add pi.has_add, zero_add := _, add_zero := _}
Equations
- pi.add_monoid = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (x : Π (i : I), f i) (i : I), n • x i, nsmul_zero' := _, nsmul_succ' := _}
Equations
- pi.monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := λ (n : ℕ) (x : Π (i : I), f i) (i : I), x i ^ n, npow_zero' := _, npow_succ' := _}
Equations
- pi.comm_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
Equations
- pi.add_comm_monoid = {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 := _}
Equations
- pi.div_inv_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv pi.has_inv, div := has_div.div pi.has_div, div_eq_mul_inv := _, zpow := λ (z : ℤ) (x : Π (i : I), f i) (i : I), x i ^ z, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}
Equations
- pi.sub_neg_monoid = {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 := has_sub.sub pi.has_sub, sub_eq_add_neg := _, zsmul := λ (z : ℤ) (x : Π (i : I), f i) (i : I), z • x i, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _}
Equations
- pi.has_involutive_neg = {neg := has_neg.neg pi.has_neg, neg_neg := _}
Equations
- pi.has_involutive_inv = {inv := has_inv.inv pi.has_inv, inv_inv := _}
Equations
- pi.division_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv pi.has_inv, div := has_div.div pi.has_div, div_eq_mul_inv := _, zpow := λ (z : ℤ) (x : Π (i : I), f i) (i : I), x i ^ z, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _}
Equations
- pi.subtraction_monoid = {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 := has_sub.sub pi.has_sub, sub_eq_add_neg := _, zsmul := λ (z : ℤ) (x : Π (i : I), f i) (i : I), z • x i, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _}
Equations
- pi.division_comm_monoid = {mul := division_monoid.mul pi.division_monoid, mul_assoc := _, one := division_monoid.one pi.division_monoid, one_mul := _, mul_one := _, npow := division_monoid.npow pi.division_monoid, npow_zero' := _, npow_succ' := _, inv := division_monoid.inv pi.division_monoid, div := division_monoid.div pi.division_monoid, div_eq_mul_inv := _, zpow := division_monoid.zpow pi.division_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _, mul_comm := _}
Equations
- pi.subtraction_comm_monoid = {add := subtraction_monoid.add pi.subtraction_monoid, add_assoc := _, zero := subtraction_monoid.zero pi.subtraction_monoid, zero_add := _, add_zero := _, nsmul := subtraction_monoid.nsmul pi.subtraction_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := subtraction_monoid.neg pi.subtraction_monoid, sub := subtraction_monoid.sub pi.subtraction_monoid, sub_eq_add_neg := _, zsmul := subtraction_monoid.zsmul pi.subtraction_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _, add_comm := _}
Equations
- pi.add_group = {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 := has_sub.sub pi.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul pi.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
Equations
- pi.group = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv pi.has_inv, div := has_div.div pi.has_div, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow pi.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
Equations
- pi.add_comm_group = {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 := has_sub.sub pi.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul pi.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
Equations
- pi.comm_group = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv pi.has_inv, div := has_div.div pi.has_div, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow pi.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
Equations
- pi.add_left_cancel_semigroup = {add := has_add.add pi.has_add, add_assoc := _, add_left_cancel := _}
Equations
- pi.left_cancel_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_left_cancel := _}
Equations
- pi.right_cancel_semigroup = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_right_cancel := _}
Equations
- pi.add_right_cancel_semigroup = {add := has_add.add pi.has_add, add_assoc := _, add_right_cancel := _}
Equations
- pi.add_left_cancel_monoid = {add := has_add.add pi.has_add, add_assoc := _, add_left_cancel := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _}
Equations
- pi.left_cancel_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_left_cancel := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _}
Equations
- pi.add_right_cancel_monoid = {add := has_add.add pi.has_add, add_assoc := _, add_right_cancel := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _}
Equations
- pi.right_cancel_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_right_cancel := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _}
Equations
- pi.add_cancel_monoid = {add := has_add.add pi.has_add, add_assoc := _, add_left_cancel := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_right_cancel := _}
Equations
- pi.cancel_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_left_cancel := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, mul_right_cancel := _}
Equations
- pi.cancel_comm_monoid = {mul := has_mul.mul pi.has_mul, mul_assoc := _, mul_left_cancel := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
Equations
- pi.add_cancel_comm_monoid = {add := has_add.add pi.has_add, add_assoc := _, add_left_cancel := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul pi.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Equations
- pi.mul_zero_class = {mul := has_mul.mul pi.has_mul, zero := 0, zero_mul := _, mul_zero := _}
Equations
- pi.mul_zero_one_class = {one := 1, mul := has_mul.mul pi.has_mul, one_mul := _, mul_one := _, zero := 0, zero_mul := _, mul_zero := _}
Equations
- pi.monoid_with_zero = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, zero := 0, zero_mul := _, mul_zero := _}
Equations
- pi.comm_monoid_with_zero = {mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow pi.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := 0, zero_mul := _, mul_zero := _}
Evaluation of functions into an indexed collection of semigroups at a point is a semigroup
homomorphism.
This is function.eval i
as a mul_hom
.
Equations
- pi.eval_mul_hom f i = {to_fun := λ (g : Π (i : I), f i), g i, map_mul' := _}
Evaluation of functions into an indexed collection of additive semigroups at a
point is an additive semigroup homomorphism.
This is function.eval i
as an add_hom
.
Equations
- pi.eval_add_hom f i = {to_fun := λ (g : Π (i : I), f i), g i, map_add' := _}
function.const
as a mul_hom
.
Equations
- pi.const_mul_hom α β = {to_fun := function.const α, map_mul' := _}
function.const
as an add_hom
.
Equations
- pi.const_add_hom α β = {to_fun := function.const α, map_add' := _}
Coercion of a mul_hom
into a function is itself a mul_hom
.
See also mul_hom.eval
.
Coercion of an add_hom
into a function is itself a add_hom
.
See also add_hom.eval
.
Additive semigroup homomorphism between the function spaces I → α
and I → β
,
induced by an additive semigroup homomorphism f
between α
and β
Semigroup homomorphism between the function spaces I → α
and I → β
, induced by a semigroup
homomorphism f
between α
and β
.
Evaluation of functions into an indexed collection of additive monoids at a
point is an additive monoid homomorphism.
This is function.eval i
as an add_monoid_hom
.
Evaluation of functions into an indexed collection of monoids at a point is a monoid
homomorphism.
This is function.eval i
as a monoid_hom
.
function.const
as an add_monoid_hom
.
Equations
- pi.const_add_monoid_hom α β = {to_fun := function.const α, map_zero' := _, map_add' := _}
function.const
as a monoid_hom
.
Equations
- pi.const_monoid_hom α β = {to_fun := function.const α, map_one' := _, map_mul' := _}
Coercion of a monoid_hom
into a function is itself a monoid_hom
.
See also monoid_hom.eval
.
Coercion of an add_monoid_hom
into a function is itself a add_monoid_hom
.
See also add_monoid_hom.eval
.
Additive monoid homomorphism between the function spaces I → α
and I → β
,
induced by an additive monoid homomorphism f
between α
and β
Monoid homomorphism between the function spaces I → α
and I → β
, induced by a monoid
homomorphism f
between α
and β
.
The one-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.
This is the one_hom
version of pi.mul_single
.
Equations
- one_hom.single f i = {to_fun := pi.mul_single i, map_one' := _}
The zero-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.
The monoid homomorphism including a single monoid into a dependent family of additive monoids, as functions supported at a point.
This is the monoid_hom
version of pi.mul_single
.
Equations
- monoid_hom.single f i = {to_fun := (one_hom.single f i).to_fun, map_one' := _, map_mul' := _}
The additive monoid homomorphism including a single additive monoid into a dependent family of additive monoids, as functions supported at a point.
This is the add_monoid_hom
version of pi.single
.
Equations
- add_monoid_hom.single f i = {to_fun := (zero_hom.single f i).to_fun, map_zero' := _, map_add' := _}
The multiplicative homomorphism including a single mul_zero_class
into a dependent family of mul_zero_class
es, as functions supported at a point.
The injection into a pi group at different indices commutes.
For injections of commuting elements at the same index, see commute.map
The injection into an additive pi group at different indices commutes.
For injections of commuting elements at the same index, see add_commute.map
The injection into a pi group with the same values commutes.
The injection into an additive pi group with the same values commutes.
function.extend s f 0
as a bundled hom.
Equations
- function.extend_by_zero.hom R s = {to_fun := λ (f : ι → R), function.extend s f 0, map_zero' := _, map_add' := _}
function.extend s f 1
as a bundled hom.
Equations
- function.extend_by_one.hom R s = {to_fun := λ (f : ι → R), function.extend s f 1, map_one' := _, map_mul' := _}