Type tags that turn additive structures into multiplicative, and vice versa #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define two type tags:
additive α
: turns any multiplicative structure onα
into the corresponding additive structure onadditive α
;multiplicative α
: turns any additive structure onα
into the corresponding multiplicative structure onmultiplicative α
.
We also define instances additive.*
and multiplicative.*
that actually transfer the structures.
See also #
This file is similar to order.synonym
.
If α
carries some multiplicative structure, then additive α
carries the corresponding
additive structure.
Instances for additive
- additive.inhabited
- additive.finite
- additive.infinite
- additive.nontrivial
- additive.has_add
- additive.add_semigroup
- additive.add_comm_semigroup
- additive.is_left_cancel_add
- additive.is_right_cancel_add
- additive.is_cancel_add
- additive.add_left_cancel_semigroup
- additive.add_right_cancel_semigroup
- additive.has_zero
- additive.add_zero_class
- additive.add_monoid
- additive.add_left_cancel_monoid
- additive.add_right_cancel_monoid
- additive.add_comm_monoid
- additive.has_neg
- additive.has_sub
- additive.has_involutive_neg
- additive.sub_neg_monoid
- additive.subtraction_monoid
- additive.subtraction_comm_monoid
- additive.add_group
- additive.add_comm_group
- additive.has_coe_to_fun
- add_action.function_End
- additive.has_vadd
- additive.add_action
- additive.add_action_is_pretransitive
- additive.vadd_comm_class
- additive.has_le
- additive.has_lt
- additive.preorder
- additive.partial_order
- additive.linear_order
- additive.order_bot
- additive.order_top
- additive.bounded_order
- additive.ordered_add_comm_monoid
- additive.ordered_cancel_add_comm_monoid
- additive.linear_ordered_add_comm_monoid
- additive.has_exists_add_of_le
- additive.canonically_ordered_add_monoid
- additive.canonically_linear_ordered_add_monoid
- additive.linear_ordered_add_comm_monoid_with_top
- additive.linear_ordered_add_comm_group_with_top
- additive.fintype
- additive.ordered_add_comm_group
- additive.linear_ordered_add_comm_group
- additive.topological_space
- additive.discrete_topology
- additive.uniform_space
- additive.has_continuous_add
- additive.has_continuous_neg
- additive.topological_add_group
- additive.has_edist
- additive.pseudo_emetric_space
- additive.emetric_space
- additive.bornology
- additive.bounded_space
- additive.has_dist
- additive.pseudo_metric_space
- additive.metric_space
- additive.proper_space
- additive.has_lipschitz_add
- additive.has_isometric_vadd
- additive.has_isometric_vadd'
- additive.has_isometric_vadd''
- additive.has_norm
- additive.has_nnnorm
- additive.seminormed_add_group
- additive.seminormed_add_comm_group
- additive.normed_add_group
- additive.normed_add_comm_group
- add_monoid.fg_of_monoid_fg
- add_group.fg_of_group_fg
- additive.normed_ordered_add_group
- additive.normed_linear_ordered_add_group
- additive.unique_sums
If α
carries some additive structure, then multiplicative α
carries the corresponding
multiplicative structure.
Equations
- multiplicative α = α
Instances for multiplicative
- multiplicative.inhabited
- multiplicative.finite
- multiplicative.infinite
- multiplicative.nontrivial
- multiplicative.has_mul
- multiplicative.semigroup
- multiplicative.comm_semigroup
- multiplicative.is_left_cancel_mul
- multiplicative.is_right_cancel_mul
- multiplicative.is_cancel_mul
- multiplicative.left_cancel_semigroup
- multiplicative.right_cancel_semigroup
- multiplicative.has_one
- multiplicative.mul_one_class
- multiplicative.monoid
- multiplicative.left_cancel_monoid
- multiplicative.right_cancel_monoid
- multiplicative.comm_monoid
- multiplicative.has_inv
- multiplicative.has_div
- multiplicative.has_involutive_inv
- multiplicative.div_inv_monoid
- multiplicative.division_monoid
- multiplicative.division_comm_monoid
- multiplicative.group
- multiplicative.comm_group
- multiplicative.has_coe_to_fun
- multiplicative.has_smul
- multiplicative.mul_action
- multiplicative.add_action_is_pretransitive
- multiplicative.smul_comm_class
- multiplicative.has_le
- multiplicative.has_lt
- multiplicative.preorder
- multiplicative.partial_order
- multiplicative.linear_order
- multiplicative.order_bot
- multiplicative.order_top
- multiplicative.bounded_order
- multiplicative.ordered_comm_monoid
- multiplicative.ordered_cancel_comm_monoid
- multiplicative.linear_ordered_comm_monoid
- multiplicative.has_exists_mul_of_le
- multiplicative.canonically_ordered_monoid
- multiplicative.canonically_linear_ordered_monoid
- multiplicative.linear_ordered_comm_monoid_with_zero
- multiplicative.linear_ordered_comm_group_with_zero
- multiplicative.fintype
- multiplicative.ordered_comm_group
- multiplicative.linear_ordered_comm_group
- multiplicative.topological_space
- multiplicative.discrete_topology
- multiplicative.uniform_space
- multiplicative.has_continuous_mul
- multiplicative.has_continuous_inv
- multiplicative.topological_group
- multiplicative.has_edist
- multiplicative.pseudo_emetric_space
- multiplicative.emetric_space
- multiplicative.bornology
- multiplicative.bounded_space
- multiplicative.has_dist
- multiplicative.pseudo_metric_space
- multiplicative.metric_space
- multiplicative.proper_space
- multiplicative.has_lipschitz_mul
- multiplicative.has_isometric_smul
- multiplicative.has_isometric_smul'
- multiplicative.has_isometric_vadd''
- multiplicative.has_norm
- multiplicative.has_nnnorm
- multiplicative.seminormed_group
- multiplicative.seminormed_comm_group
- multiplicative.normed_group
- multiplicative.normed_comm_group
- monoid.fg_of_add_monoid_fg
- group.fg_of_mul_group_fg
- multiplicative.normed_ordered_group
- multiplicative.normed_linear_ordered_group
- multiplicative.unique_prods
- add_char.monoid_hom_class
Reinterpret x : additive α
as an element of α
.
Equations
Reinterpret x : α
as an element of multiplicative α
.
Equations
- multiplicative.of_add = {to_fun := λ (x : α), x, inv_fun := λ (x : multiplicative α), x, left_inv := _, right_inv := _}
Reinterpret x : multiplicative α
as an element of α
.
Equations
Equations
Equations
Equations
- additive.has_add = {add := λ (x y : additive α), ⇑additive.of_mul (⇑additive.to_mul x * ⇑additive.to_mul y)}
Equations
- multiplicative.has_mul = {mul := λ (x y : multiplicative α), ⇑multiplicative.of_add (⇑multiplicative.to_add x + ⇑multiplicative.to_add y)}
Equations
Equations
Equations
- additive.add_comm_semigroup = {add := add_semigroup.add additive.add_semigroup, add_assoc := _, add_comm := _}
Equations
- multiplicative.comm_semigroup = {mul := semigroup.mul multiplicative.semigroup, mul_assoc := _, mul_comm := _}
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- additive.add_zero_class = {zero := 0, add := has_add.add additive.has_add, zero_add := _, add_zero := _}
Equations
- multiplicative.mul_one_class = {one := 1, mul := has_mul.mul multiplicative.has_mul, one_mul := _, mul_one := _}
Equations
- additive.add_monoid = {add := has_add.add additive.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := monoid.npow h, nsmul_zero' := _, nsmul_succ' := _}
Equations
- multiplicative.monoid = {mul := has_mul.mul multiplicative.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := add_monoid.nsmul h, npow_zero' := _, npow_succ' := _}
Equations
- additive.add_left_cancel_monoid = {add := has_add.add additive.has_add, add_assoc := _, add_left_cancel := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul additive.add_monoid, nsmul_zero' := _, nsmul_succ' := _}
Equations
- multiplicative.left_cancel_monoid = {mul := has_mul.mul multiplicative.has_mul, mul_assoc := _, mul_left_cancel := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow multiplicative.monoid, npow_zero' := _, npow_succ' := _}
Equations
- additive.add_right_cancel_monoid = {add := has_add.add additive.has_add, add_assoc := _, add_right_cancel := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul additive.add_monoid, nsmul_zero' := _, nsmul_succ' := _}
Equations
- multiplicative.right_cancel_monoid = {mul := has_mul.mul multiplicative.has_mul, mul_assoc := _, mul_right_cancel := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow multiplicative.monoid, npow_zero' := _, npow_succ' := _}
Equations
- additive.add_comm_monoid = {add := has_add.add additive.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul additive.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Equations
- multiplicative.comm_monoid = {mul := has_mul.mul multiplicative.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow multiplicative.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
Equations
- additive.has_neg = {neg := λ (x : additive α), ⇑multiplicative.of_add (⇑additive.to_mul x)⁻¹}
Equations
- multiplicative.has_inv = {inv := λ (x : multiplicative α), ⇑additive.of_mul (-⇑multiplicative.to_add x)}
Equations
- additive.has_sub = {sub := λ (x y : additive α), ⇑additive.of_mul (⇑additive.to_mul x / ⇑additive.to_mul y)}
Equations
- multiplicative.has_div = {div := λ (x y : multiplicative α), ⇑multiplicative.of_add (⇑multiplicative.to_add x - ⇑multiplicative.to_add y)}
Equations
Equations
Equations
- additive.sub_neg_monoid = {add := add_monoid.add additive.add_monoid, add_assoc := _, zero := add_monoid.zero additive.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul additive.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg additive.has_neg, sub := has_sub.sub additive.has_sub, sub_eq_add_neg := _, zsmul := div_inv_monoid.zpow _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _}
Equations
- multiplicative.div_inv_monoid = {mul := monoid.mul multiplicative.monoid, mul_assoc := _, one := monoid.one multiplicative.monoid, one_mul := _, mul_one := _, npow := monoid.npow multiplicative.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv multiplicative.has_inv, div := has_div.div multiplicative.has_div, div_eq_mul_inv := _, zpow := sub_neg_monoid.zsmul _inst_1, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}
Equations
- additive.subtraction_monoid = {add := sub_neg_monoid.add additive.sub_neg_monoid, add_assoc := _, zero := sub_neg_monoid.zero additive.sub_neg_monoid, zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul additive.sub_neg_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg additive.sub_neg_monoid, sub := sub_neg_monoid.sub additive.sub_neg_monoid, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul additive.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _}
Equations
- multiplicative.division_monoid = {mul := div_inv_monoid.mul multiplicative.div_inv_monoid, mul_assoc := _, one := div_inv_monoid.one multiplicative.div_inv_monoid, one_mul := _, mul_one := _, npow := div_inv_monoid.npow multiplicative.div_inv_monoid, npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv multiplicative.div_inv_monoid, div := div_inv_monoid.div multiplicative.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow multiplicative.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _}
Equations
- additive.subtraction_comm_monoid = {add := subtraction_monoid.add additive.subtraction_monoid, add_assoc := _, zero := subtraction_monoid.zero additive.subtraction_monoid, zero_add := _, add_zero := _, nsmul := subtraction_monoid.nsmul additive.subtraction_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := subtraction_monoid.neg additive.subtraction_monoid, sub := subtraction_monoid.sub additive.subtraction_monoid, sub_eq_add_neg := _, zsmul := subtraction_monoid.zsmul additive.subtraction_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _, add_comm := _}
Equations
- multiplicative.division_comm_monoid = {mul := division_monoid.mul multiplicative.division_monoid, mul_assoc := _, one := division_monoid.one multiplicative.division_monoid, one_mul := _, mul_one := _, npow := division_monoid.npow multiplicative.division_monoid, npow_zero' := _, npow_succ' := _, inv := division_monoid.inv multiplicative.division_monoid, div := division_monoid.div multiplicative.division_monoid, div_eq_mul_inv := _, zpow := division_monoid.zpow multiplicative.division_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _, mul_comm := _}
Equations
- additive.add_group = {add := sub_neg_monoid.add additive.sub_neg_monoid, add_assoc := _, zero := sub_neg_monoid.zero additive.sub_neg_monoid, zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul additive.sub_neg_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg additive.sub_neg_monoid, sub := sub_neg_monoid.sub additive.sub_neg_monoid, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul additive.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
Equations
- multiplicative.group = {mul := div_inv_monoid.mul multiplicative.div_inv_monoid, mul_assoc := _, one := div_inv_monoid.one multiplicative.div_inv_monoid, one_mul := _, mul_one := _, npow := div_inv_monoid.npow multiplicative.div_inv_monoid, npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv multiplicative.div_inv_monoid, div := div_inv_monoid.div multiplicative.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow multiplicative.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
Equations
- additive.add_comm_group = {add := add_group.add additive.add_group, add_assoc := _, zero := add_group.zero additive.add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul additive.add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg additive.add_group, sub := add_group.sub additive.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul additive.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
Equations
- multiplicative.comm_group = {mul := group.mul multiplicative.group, mul_assoc := _, one := group.one multiplicative.group, one_mul := _, mul_one := _, npow := group.npow multiplicative.group, npow_zero' := _, npow_succ' := _, inv := group.inv multiplicative.group, div := group.div multiplicative.group, div_eq_mul_inv := _, zpow := group.zpow multiplicative.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
Reinterpret α →+ β
as multiplicative α →* multiplicative β
.
Equations
- add_monoid_hom.to_multiplicative = {to_fun := λ (f : α →+ β), {to_fun := λ (a : multiplicative α), ⇑multiplicative.of_add (⇑f (⇑multiplicative.to_add a)), map_one' := _, map_mul' := _}, inv_fun := λ (f : multiplicative α →* multiplicative β), {to_fun := λ (a : α), ⇑multiplicative.to_add (⇑f (⇑multiplicative.of_add a)), map_zero' := _, map_add' := _}, left_inv := _, right_inv := _}
Reinterpret α →* β
as additive α →+ additive β
.
Equations
- monoid_hom.to_additive = {to_fun := λ (f : α →* β), {to_fun := λ (a : additive α), ⇑additive.of_mul (⇑f (⇑additive.to_mul a)), map_zero' := _, map_add' := _}, inv_fun := λ (f : additive α →+ additive β), {to_fun := λ (a : α), ⇑additive.to_mul (⇑f (⇑additive.of_mul a)), map_one' := _, map_mul' := _}, left_inv := _, right_inv := _}
Reinterpret additive α →+ β
as α →* multiplicative β
.
Equations
- add_monoid_hom.to_multiplicative' = {to_fun := λ (f : additive α →+ β), {to_fun := λ (a : α), ⇑multiplicative.of_add (⇑f (⇑additive.of_mul a)), map_one' := _, map_mul' := _}, inv_fun := λ (f : α →* multiplicative β), {to_fun := λ (a : additive α), ⇑multiplicative.to_add (⇑f (⇑additive.to_mul a)), map_zero' := _, map_add' := _}, left_inv := _, right_inv := _}
Reinterpret α →* multiplicative β
as additive α →+ β
.
Reinterpret α →+ additive β
as multiplicative α →* β
.
Equations
- add_monoid_hom.to_multiplicative'' = {to_fun := λ (f : α →+ additive β), {to_fun := λ (a : multiplicative α), ⇑additive.to_mul (⇑f (⇑multiplicative.to_add a)), map_one' := _, map_mul' := _}, inv_fun := λ (f : multiplicative α →* β), {to_fun := λ (a : α), ⇑additive.of_mul (⇑f (⇑multiplicative.of_add a)), map_zero' := _, map_add' := _}, left_inv := _, right_inv := _}
Reinterpret multiplicative α →* β
as α →+ additive β
.
If α
has some multiplicative structure and coerces to a function,
then additive α
should also coerce to the same function.
This allows additive
to be used on bundled function types with a multiplicative structure, which
is often used for composition, without affecting the behavior of the function itself.
Equations
- additive.has_coe_to_fun = {coe := λ (a : additive α), ⇑(⇑additive.to_mul a)}
If α
has some additive structure and coerces to a function,
then multiplicative α
should also coerce to the same function.
This allows multiplicative
to be used on bundled function types with an additive structure, which
is often used for composition, without affecting the behavior of the function itself.
Equations
- multiplicative.has_coe_to_fun = {coe := λ (a : multiplicative α), ⇑(⇑multiplicative.to_add a)}