mathlib documentation

algebra.group.type_tags

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 on additive α;
multiplicative α: turns any additive structure on α into the corresponding multiplicative structure on multiplicative α.

We also define instances additive.* and multiplicative.* that actually transfer the structures.

See also #

This file is similar to order.synonym.

def additive (α : Type u_1) :

Type u_1

If α carries some multiplicative structure, then additive α carries the corresponding additive structure.

Equations

additive α = α

Instances for additive

def multiplicative (α : Type u_1) :

Type u_1

If α carries some additive structure, then multiplicative α carries the corresponding multiplicative structure.

Equations

multiplicative α = α

Instances for multiplicative

def additive.of_mul {α : Type u} :

α ≃ additive α

Reinterpret x : α as an element of additive α.

Equations

additive.of_mul = {to_fun := λ (x : α), x, inv_fun := λ (x : additive α), x, left_inv := _, right_inv := _}

def additive.to_mul {α : Type u} :

additive α ≃ α

Reinterpret x : additive α as an element of α.

Equations

additive.to_mul = additive.of_mul.symm

@[simp]

theorem additive.of_mul_symm_eq {α : Type u} :

additive.of_mul.symm = additive.to_mul

@[simp]

theorem additive.to_mul_symm_eq {α : Type u} :

additive.to_mul.symm = additive.of_mul

def multiplicative.of_add {α : Type u} :

α ≃ multiplicative α

Reinterpret x : α as an element of multiplicative α.

Equations

multiplicative.of_add = {to_fun := λ (x : α), x, inv_fun := λ (x : multiplicative α), x, left_inv := _, right_inv := _}

def multiplicative.to_add {α : Type u} :

multiplicative α ≃ α

Reinterpret x : multiplicative α as an element of α.

Equations

multiplicative.to_add = multiplicative.of_add.symm

@[simp]

theorem multiplicative.of_add_symm_eq {α : Type u} :

multiplicative.of_add.symm = multiplicative.to_add

@[simp]

theorem multiplicative.to_add_symm_eq {α : Type u} :

multiplicative.to_add.symm = multiplicative.of_add

@[simp]

theorem to_add_of_add {α : Type u} (x : α) :

⇑multiplicative.to_add (⇑multiplicative.of_add x) = x

@[simp]

theorem of_add_to_add {α : Type u} (x : multiplicative α) :

⇑multiplicative.of_add (⇑multiplicative.to_add x) = x

@[simp]

theorem to_mul_of_mul {α : Type u} (x : α) :

⇑additive.to_mul (⇑additive.of_mul x) = x

@[simp]

theorem of_mul_to_mul {α : Type u} (x : additive α) :

⇑additive.of_mul (⇑additive.to_mul x) = x

@[protected, instance]

def additive.inhabited {α : Type u} [inhabited α] :

inhabited (additive α)

Equations

additive.inhabited = {default := ⇑additive.of_mul inhabited.default}

@[protected, instance]

def multiplicative.inhabited {α : Type u} [inhabited α] :

inhabited (multiplicative α)

Equations

multiplicative.inhabited = {default := ⇑multiplicative.of_add inhabited.default}

@[protected, instance]

def additive.finite {α : Type u} [finite α] :

finite (additive α)

@[protected, instance]

def multiplicative.finite {α : Type u} [finite α] :

finite (multiplicative α)

@[protected, instance]

def additive.infinite {α : Type u} [infinite α] :

infinite (additive α)

@[protected, instance]

def multiplicative.infinite {α : Type u} [infinite α] :

infinite (multiplicative α)

@[protected, instance]

def additive.nontrivial {α : Type u} [nontrivial α] :

nontrivial (additive α)

@[protected, instance]

def multiplicative.nontrivial {α : Type u} [nontrivial α] :

nontrivial (multiplicative α)

@[protected, instance]

def additive.has_add {α : Type u} [has_mul α] :

has_add (additive α)

Equations

additive.has_add = {add := λ (x y : additive α), ⇑additive.of_mul (⇑additive.to_mul x * ⇑additive.to_mul y)}

@[protected, instance]

def multiplicative.has_mul {α : Type u} [has_add α] :

has_mul (multiplicative α)

Equations

multiplicative.has_mul = {mul := λ (x y : multiplicative α), ⇑multiplicative.of_add (⇑multiplicative.to_add x + ⇑multiplicative.to_add y)}

@[simp]

theorem of_add_add {α : Type u} [has_add α] (x y : α) :

⇑multiplicative.of_add (x + y) = ⇑multiplicative.of_add x * ⇑multiplicative.of_add y

@[simp]

theorem to_add_mul {α : Type u} [has_add α] (x y : multiplicative α) :

⇑multiplicative.to_add (x * y) = ⇑multiplicative.to_add x + ⇑multiplicative.to_add y

@[simp]

theorem of_mul_mul {α : Type u} [has_mul α] (x y : α) :

⇑additive.of_mul (x * y) = ⇑additive.of_mul x + ⇑additive.of_mul y

@[simp]

theorem to_mul_add {α : Type u} [has_mul α] (x y : additive α) :

⇑additive.to_mul (x + y) = ⇑additive.to_mul x * ⇑additive.to_mul y

@[protected, instance]

def additive.add_semigroup {α : Type u} [semigroup α] :

add_semigroup (additive α)

Equations

additive.add_semigroup = {add := has_add.add additive.has_add, add_assoc := _}

@[protected, instance]

def multiplicative.semigroup {α : Type u} [add_semigroup α] :

semigroup (multiplicative α)

Equations

multiplicative.semigroup = {mul := has_mul.mul multiplicative.has_mul, mul_assoc := _}

@[protected, instance]

def additive.add_comm_semigroup {α : Type u} [comm_semigroup α] :

add_comm_semigroup (additive α)

Equations

additive.add_comm_semigroup = {add := add_semigroup.add additive.add_semigroup, add_assoc := _, add_comm := _}

@[protected, instance]

def multiplicative.comm_semigroup {α : Type u} [add_comm_semigroup α] :

comm_semigroup (multiplicative α)

Equations

multiplicative.comm_semigroup = {mul := semigroup.mul multiplicative.semigroup, mul_assoc := _, mul_comm := _}

@[protected, instance]

def additive.is_left_cancel_add {α : Type u} [has_mul α] [is_left_cancel_mul α] :

is_left_cancel_add (additive α)

@[protected, instance]

def multiplicative.is_left_cancel_mul {α : Type u} [has_add α] [is_left_cancel_add α] :

is_left_cancel_mul (multiplicative α)

@[protected, instance]

def additive.is_right_cancel_add {α : Type u} [has_mul α] [is_right_cancel_mul α] :

is_right_cancel_add (additive α)

@[protected, instance]

def multiplicative.is_right_cancel_mul {α : Type u} [has_add α] [is_right_cancel_add α] :

is_right_cancel_mul (multiplicative α)

@[protected, instance]

def additive.is_cancel_add {α : Type u} [has_mul α] [is_cancel_mul α] :

is_cancel_add (additive α)

@[protected, instance]

def multiplicative.is_cancel_mul {α : Type u} [has_add α] [is_cancel_add α] :

is_cancel_mul (multiplicative α)

@[protected, instance]

def additive.add_left_cancel_semigroup {α : Type u} [left_cancel_semigroup α] :

add_left_cancel_semigroup (additive α)

Equations

additive.add_left_cancel_semigroup = {add := add_semigroup.add additive.add_semigroup, add_assoc := _, add_left_cancel := _}

@[protected, instance]

def multiplicative.left_cancel_semigroup {α : Type u} [add_left_cancel_semigroup α] :

left_cancel_semigroup (multiplicative α)

Equations

multiplicative.left_cancel_semigroup = {mul := semigroup.mul multiplicative.semigroup, mul_assoc := _, mul_left_cancel := _}

@[protected, instance]

def additive.add_right_cancel_semigroup {α : Type u} [right_cancel_semigroup α] :

add_right_cancel_semigroup (additive α)

Equations

additive.add_right_cancel_semigroup = {add := add_semigroup.add additive.add_semigroup, add_assoc := _, add_right_cancel := _}

@[protected, instance]

def multiplicative.right_cancel_semigroup {α : Type u} [add_right_cancel_semigroup α] :

right_cancel_semigroup (multiplicative α)

Equations

multiplicative.right_cancel_semigroup = {mul := semigroup.mul multiplicative.semigroup, mul_assoc := _, mul_right_cancel := _}

@[protected, instance]

def additive.has_zero {α : Type u} [has_one α] :

has_zero (additive α)

Equations

additive.has_zero = {zero := ⇑additive.of_mul 1}

@[simp]

theorem of_mul_one {α : Type u} [has_one α] :

⇑additive.of_mul 1 = 0

@[simp]

theorem of_mul_eq_zero {A : Type u_1} [has_one A] {x : A} :

⇑additive.of_mul x = 0 ↔ x = 1

@[simp]

theorem to_mul_zero {α : Type u} [has_one α] :

⇑additive.to_mul 0 = 1

@[protected, instance]

def multiplicative.has_one {α : Type u} [has_zero α] :

has_one (multiplicative α)

Equations

multiplicative.has_one = {one := ⇑multiplicative.of_add 0}

@[simp]

theorem of_add_zero {α : Type u} [has_zero α] :

⇑multiplicative.of_add 0 = 1

@[simp]

theorem of_add_eq_one {A : Type u_1} [has_zero A] {x : A} :

⇑multiplicative.of_add x = 1 ↔ x = 0

@[simp]

theorem to_add_one {α : Type u} [has_zero α] :

⇑multiplicative.to_add 1 = 0

@[protected, instance]

def additive.add_zero_class {α : Type u} [mul_one_class α] :

add_zero_class (additive α)

Equations

additive.add_zero_class = {zero := 0, add := has_add.add additive.has_add, zero_add := _, add_zero := _}

@[protected, instance]

def multiplicative.mul_one_class {α : Type u} [add_zero_class α] :

mul_one_class (multiplicative α)

Equations

multiplicative.mul_one_class = {one := 1, mul := has_mul.mul multiplicative.has_mul, one_mul := _, mul_one := _}

@[protected, instance]

def additive.add_monoid {α : Type u} [h : monoid α] :

add_monoid (additive α)

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' := _}

@[protected, instance]

def multiplicative.monoid {α : Type u} [h : add_monoid α] :

monoid (multiplicative α)

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' := _}

@[protected, instance]

def additive.add_left_cancel_monoid {α : Type u} [left_cancel_monoid α] :

add_left_cancel_monoid (additive α)

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' := _}

@[protected, instance]

def multiplicative.left_cancel_monoid {α : Type u} [add_left_cancel_monoid α] :

left_cancel_monoid (multiplicative α)

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' := _}

@[protected, instance]

def additive.add_right_cancel_monoid {α : Type u} [right_cancel_monoid α] :

add_right_cancel_monoid (additive α)

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' := _}

@[protected, instance]

def multiplicative.right_cancel_monoid {α : Type u} [add_right_cancel_monoid α] :

right_cancel_monoid (multiplicative α)

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' := _}

@[protected, instance]

def additive.add_comm_monoid {α : Type u} [comm_monoid α] :

add_comm_monoid (additive α)

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 := _}

@[protected, instance]

def multiplicative.comm_monoid {α : Type u} [add_comm_monoid α] :

comm_monoid (multiplicative α)

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 := _}

@[protected, instance]

def additive.has_neg {α : Type u} [has_inv α] :

has_neg (additive α)

Equations

additive.has_neg = {neg := λ (x : additive α), ⇑multiplicative.of_add (⇑additive.to_mul x)⁻¹}

@[simp]

theorem of_mul_inv {α : Type u} [has_inv α] (x : α) :

⇑additive.of_mul x⁻¹ = -⇑additive.of_mul x

@[simp]

theorem to_mul_neg {α : Type u} [has_inv α] (x : additive α) :

⇑additive.to_mul (-x) = (⇑additive.to_mul x)⁻¹

@[protected, instance]

def multiplicative.has_inv {α : Type u} [has_neg α] :

has_inv (multiplicative α)

Equations

multiplicative.has_inv = {inv := λ (x : multiplicative α), ⇑additive.of_mul (-⇑multiplicative.to_add x)}

@[simp]

theorem of_add_neg {α : Type u} [has_neg α] (x : α) :

⇑multiplicative.of_add (-x) = (⇑multiplicative.of_add x)⁻¹

@[simp]

theorem to_add_inv {α : Type u} [has_neg α] (x : multiplicative α) :

⇑multiplicative.to_add x⁻¹ = -⇑multiplicative.to_add x

@[protected, instance]

def additive.has_sub {α : Type u} [has_div α] :

has_sub (additive α)

Equations

additive.has_sub = {sub := λ (x y : additive α), ⇑additive.of_mul (⇑additive.to_mul x / ⇑additive.to_mul y)}

@[protected, instance]

def multiplicative.has_div {α : Type u} [has_sub α] :

has_div (multiplicative α)

Equations

multiplicative.has_div = {div := λ (x y : multiplicative α), ⇑multiplicative.of_add (⇑multiplicative.to_add x - ⇑multiplicative.to_add y)}

@[simp]

theorem of_add_sub {α : Type u} [has_sub α] (x y : α) :

⇑multiplicative.of_add (x - y) = ⇑multiplicative.of_add x / ⇑multiplicative.of_add y

@[simp]

theorem to_add_div {α : Type u} [has_sub α] (x y : multiplicative α) :

⇑multiplicative.to_add (x / y) = ⇑multiplicative.to_add x - ⇑multiplicative.to_add y

@[simp]

theorem of_mul_div {α : Type u} [has_div α] (x y : α) :

⇑additive.of_mul (x / y) = ⇑additive.of_mul x - ⇑additive.of_mul y

@[simp]

theorem to_mul_sub {α : Type u} [has_div α] (x y : additive α) :

⇑additive.to_mul (x - y) = ⇑additive.to_mul x / ⇑additive.to_mul y

@[protected, instance]

def additive.has_involutive_neg {α : Type u} [has_involutive_inv α] :

has_involutive_neg (additive α)

Equations

additive.has_involutive_neg = {neg := has_neg.neg additive.has_neg, neg_neg := _}

@[protected, instance]

def multiplicative.has_involutive_inv {α : Type u} [has_involutive_neg α] :

has_involutive_inv (multiplicative α)

Equations

multiplicative.has_involutive_inv = {inv := has_inv.inv multiplicative.has_inv, inv_inv := _}

@[protected, instance]

def additive.sub_neg_monoid {α : Type u} [div_inv_monoid α] :

sub_neg_monoid (additive α)

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' := _}

@[protected, instance]

def multiplicative.div_inv_monoid {α : Type u} [sub_neg_monoid α] :

div_inv_monoid (multiplicative α)

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' := _}

@[protected, instance]

def additive.subtraction_monoid {α : Type u} [division_monoid α] :

subtraction_monoid (additive α)

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 := _}

@[protected, instance]

def multiplicative.division_monoid {α : Type u} [subtraction_monoid α] :

division_monoid (multiplicative α)

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 := _}

@[protected, instance]

def additive.subtraction_comm_monoid {α : Type u} [division_comm_monoid α] :

subtraction_comm_monoid (additive α)

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 := _}

@[protected, instance]

def multiplicative.division_comm_monoid {α : Type u} [subtraction_comm_monoid α] :

division_comm_monoid (multiplicative α)

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 := _}

@[protected, instance]

def additive.add_group {α : Type u} [group α] :

add_group (additive α)

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 := _}

@[protected, instance]

def multiplicative.group {α : Type u} [add_group α] :

group (multiplicative α)

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 := _}

@[protected, instance]

def additive.add_comm_group {α : Type u} [comm_group α] :

add_comm_group (additive α)

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 := _}

@[protected, instance]

def multiplicative.comm_group {α : Type u} [add_comm_group α] :

comm_group (multiplicative α)

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 := _}

def add_monoid_hom.to_multiplicative {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] :

(α →+ β) ≃ (multiplicative α →* multiplicative β)

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 := _}

@[simp]

theorem add_monoid_hom.to_multiplicative_symm_apply_apply {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] (f : multiplicative α →* multiplicative β) (a : α) :

⇑(⇑(add_monoid_hom.to_multiplicative.symm) f) a = ⇑multiplicative.to_add (⇑f (⇑multiplicative.of_add a))

@[simp]

theorem add_monoid_hom.to_multiplicative_apply_apply {α : Type u} {β : Type v} [add_zero_class α] [add_zero_class β] (f : α →+ β) (a : multiplicative α) :

⇑(⇑add_monoid_hom.to_multiplicative f) a = ⇑multiplicative.of_add (⇑f (⇑multiplicative.to_add a))

def monoid_hom.to_additive {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] :

(α →* β) ≃ (additive α →+ additive β)

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 := _}

@[simp]

theorem monoid_hom.to_additive_symm_apply_apply {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] (f : additive α →+ additive β) (a : α) :

⇑(⇑(monoid_hom.to_additive.symm) f) a = ⇑additive.to_mul (⇑f (⇑additive.of_mul a))

@[simp]

theorem monoid_hom.to_additive_apply_apply {α : Type u} {β : Type v} [mul_one_class α] [mul_one_class β] (f : α →* β) (a : additive α) :

⇑(⇑monoid_hom.to_additive f) a = ⇑additive.of_mul (⇑f (⇑additive.to_mul a))

@[simp]

theorem add_monoid_hom.to_multiplicative'_apply_apply {α : Type u} {β : Type v} [mul_one_class α] [add_zero_class β] (f : additive α →+ β) (a : α) :

⇑(⇑add_monoid_hom.to_multiplicative' f) a = ⇑multiplicative.of_add (⇑f (⇑additive.of_mul a))

@[simp]

theorem add_monoid_hom.to_multiplicative'_symm_apply_apply {α : Type u} {β : Type v} [mul_one_class α] [add_zero_class β] (f : α →* multiplicative β) (a : additive α) :

⇑(⇑(add_monoid_hom.to_multiplicative'.symm) f) a = ⇑multiplicative.to_add (⇑f (⇑additive.to_mul a))

def add_monoid_hom.to_multiplicative' {α : Type u} {β : Type v} [mul_one_class α] [add_zero_class β] :

(additive α →+ β) ≃ (α →* multiplicative β)

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 := _}

@[simp]

theorem monoid_hom.to_additive'_apply_apply {α : Type u} {β : Type v} [mul_one_class α] [add_zero_class β] (ᾰ : α →* multiplicative β) (a : additive α) :

⇑(⇑monoid_hom.to_additive' ᾰ) a = ⇑multiplicative.to_add (⇑ᾰ (⇑additive.to_mul a))

def monoid_hom.to_additive' {α : Type u} {β : Type v} [mul_one_class α] [add_zero_class β] :

(α →* multiplicative β) ≃ (additive α →+ β)

Reinterpret α →* multiplicative β as additive α →+ β.

Equations

monoid_hom.to_additive' = add_monoid_hom.to_multiplicative'.symm

@[simp]

theorem monoid_hom.to_additive'_symm_apply_apply {α : Type u} {β : Type v} [mul_one_class α] [add_zero_class β] (ᾰ : additive α →+ β) (a : α) :

⇑(⇑(monoid_hom.to_additive'.symm) ᾰ) a = ⇑multiplicative.of_add (⇑ᾰ (⇑additive.of_mul a))

@[simp]

theorem add_monoid_hom.to_multiplicative''_symm_apply_apply {α : Type u} {β : Type v} [add_zero_class α] [mul_one_class β] (f : multiplicative α →* β) (a : α) :

⇑(⇑(add_monoid_hom.to_multiplicative''.symm) f) a = ⇑additive.of_mul (⇑f (⇑multiplicative.of_add a))

@[simp]

theorem add_monoid_hom.to_multiplicative''_apply_apply {α : Type u} {β : Type v} [add_zero_class α] [mul_one_class β] (f : α →+ additive β) (a : multiplicative α) :

⇑(⇑add_monoid_hom.to_multiplicative'' f) a = ⇑additive.to_mul (⇑f (⇑multiplicative.to_add a))

def add_monoid_hom.to_multiplicative'' {α : Type u} {β : Type v} [add_zero_class α] [mul_one_class β] :

(α →+ additive β) ≃ (multiplicative α →* β)

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 := _}

@[simp]

theorem monoid_hom.to_additive''_symm_apply_apply {α : Type u} {β : Type v} [add_zero_class α] [mul_one_class β] (ᾰ : α →+ additive β) (a : multiplicative α) :

⇑(⇑(monoid_hom.to_additive''.symm) ᾰ) a = ⇑additive.to_mul (⇑ᾰ (⇑multiplicative.to_add a))

@[simp]

theorem monoid_hom.to_additive''_apply_apply {α : Type u} {β : Type v} [add_zero_class α] [mul_one_class β] (ᾰ : multiplicative α →* β) (a : α) :

⇑(⇑monoid_hom.to_additive'' ᾰ) a = ⇑additive.of_mul (⇑ᾰ (⇑multiplicative.of_add a))

def monoid_hom.to_additive'' {α : Type u} {β : Type v} [add_zero_class α] [mul_one_class β] :

(multiplicative α →* β) ≃ (α →+ additive β)

Reinterpret multiplicative α →* β as α →+ additive β.

Equations

monoid_hom.to_additive'' = add_monoid_hom.to_multiplicative''.symm

@[protected, instance]

def additive.has_coe_to_fun {α : Type u_1} {β : α → Sort u_2} [has_coe_to_fun α β] :

has_coe_to_fun (additive α) (λ (a : additive α), β (⇑additive.to_mul a))

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)}

@[protected, instance]

def multiplicative.has_coe_to_fun {α : Type u_1} {β : α → Sort u_2} [has_coe_to_fun α β] :

has_coe_to_fun (multiplicative α) (λ (a : multiplicative α), β (⇑multiplicative.to_add 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)}