# Additive and multiplicative equivalences associated to `Multiplicative`

and `Additive`

. #

def
AddEquiv.toMultiplicative
{G : Type u_1}
{H : Type u_2}
[inst : AddZeroClass G]
[inst : AddZeroClass H]
:

G ≃+ H ≃ (Multiplicative G ≃* Multiplicative H)

Reinterpret `G ≃+ H≃+ H`

as `Multiplicative G ≃* Multiplicative H≃* Multiplicative H`

.

## Equations

- One or more equations did not get rendered due to their size.

def
MulEquiv.toAdditive
{G : Type u_1}
{H : Type u_2}
[inst : MulOneClass G]
[inst : MulOneClass H]
:

Reinterpret `G ≃* H≃* H`

as `Additive G ≃+ Additive H≃+ Additive H`

.

## Equations

- One or more equations did not get rendered due to their size.

def
AddEquiv.toMultiplicative'
{G : Type u_1}
{H : Type u_2}
[inst : MulOneClass G]
[inst : AddZeroClass H]
:

Additive G ≃+ H ≃ (G ≃* Multiplicative H)

Reinterpret `Additive G ≃+ H≃+ H`

as `G ≃* Multiplicative H≃* Multiplicative H`

.

## Equations

- One or more equations did not get rendered due to their size.

def
MulEquiv.toAdditive'
{G : Type u_1}
{H : Type u_2}
[inst : MulOneClass G]
[inst : AddZeroClass H]
:

G ≃* Multiplicative H ≃ (Additive G ≃+ H)

Reinterpret `G ≃* Multiplicative H≃* Multiplicative H`

as `Additive G ≃+ H≃+ H`

as.

## Equations

- MulEquiv.toAdditive' = Equiv.symm AddEquiv.toMultiplicative'

def
AddEquiv.toMultiplicative''
{G : Type u_1}
{H : Type u_2}
[inst : AddZeroClass G]
[inst : MulOneClass H]
:

G ≃+ Additive H ≃ (Multiplicative G ≃* H)

Reinterpret `G ≃+ Additive H≃+ Additive H`

as `Multiplicative G ≃* H≃* H`

.

## Equations

- One or more equations did not get rendered due to their size.

def
MulEquiv.toAdditive''
{G : Type u_1}
{H : Type u_2}
[inst : AddZeroClass G]
[inst : MulOneClass H]
:

Multiplicative G ≃* H ≃ (G ≃+ Additive H)

Reinterpret `Multiplicative G ≃* H≃* H`

as `G ≃+ Additive H≃+ Additive H`

as.

## Equations

- MulEquiv.toAdditive'' = Equiv.symm AddEquiv.toMultiplicative''

def
AddEquiv.additiveMultiplicative
(G : Type u_1)
[inst : AddZeroClass G]
:

Additive (Multiplicative G) ≃+ G

`Additive (Multiplicative G)`

is just `G`

.

## Equations

- AddEquiv.additiveMultiplicative G = ↑MulEquiv.toAdditive' (MulEquiv.refl (Multiplicative G))

def
MulEquiv.multiplicativeAdditive
(H : Type u_1)
[inst : MulOneClass H]
:

Multiplicative (Additive H) ≃* H

`Multiplicative (Additive H)`

is just `H`

.

## Equations

- MulEquiv.multiplicativeAdditive H = ↑AddEquiv.toMultiplicative'' (AddEquiv.refl (Additive H))