# Type tags that turn additive structures into multiplicative, and vice versa #

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`

.

## Porting notes #

- Since bundled morphism applications that rely on
`CoeFun`

currently don't work, they are ported as`toFoo a`

rather than`a.toFoo`

for now. (https://github.com/leanprover/lean4/issues/1910)

If `α`

carries some additive structure, then `Multiplicative α`

carries the corresponding
multiplicative structure.

## Equations

- Multiplicative α = α

## Instances For

Reinterpret `x : α`

as an element of `Multiplicative α`

.

## Equations

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

## Instances For

Reinterpret `x : Multiplicative α`

as an element of `α`

.

## Equations

- Multiplicative.toAdd = Multiplicative.ofAdd.symm

## Instances For

## Equations

- (_ : Subsingleton (Additive α)) = (_ : Subsingleton (Additive α))

## Equations

- (_ : Subsingleton (Multiplicative α)) = (_ : Subsingleton (Multiplicative α))

## Equations

- instInhabitedMultiplicative = { default := Multiplicative.ofAdd default }

## Equations

- instUniqueAdditive = Equiv.unique Additive.toMul

## Equations

- instUniqueMultiplicative = Equiv.unique Multiplicative.toAdd

## Equations

- (_ : Finite (Multiplicative α)) = (_ : Finite (Multiplicative α))

## Equations

- (_ : Infinite (Multiplicative α)) = h

## Equations

- instDecidableEqMultiplicative = h

## Equations

- instDecidableEqAdditive = h

## Equations

- (_ : Nontrivial (Additive α)) = (_ : Nontrivial (Additive α))

## Equations

- (_ : Nontrivial (Multiplicative α)) = (_ : Nontrivial (Multiplicative α))

## Equations

- Multiplicative.mul = { mul := fun (x y : Multiplicative α) => Multiplicative.ofAdd (Multiplicative.toAdd x + Multiplicative.toAdd y) }

## Equations

- Additive.addCommSemigroup = let src := Additive.addSemigroup; AddCommSemigroup.mk (_ : ∀ (a b : α), a * b = b * a)

## Equations

- Multiplicative.commSemigroup = let src := Multiplicative.semigroup; CommSemigroup.mk (_ : ∀ (a b : α), a + b = b + a)

## Equations

- (_ : IsLeftCancelAdd (Additive α)) = (_ : IsLeftCancelAdd (Additive α))

## Equations

- (_ : IsLeftCancelMul (Multiplicative α)) = (_ : IsLeftCancelMul (Multiplicative α))

## Equations

- (_ : IsRightCancelAdd (Additive α)) = (_ : IsRightCancelAdd (Additive α))

## Equations

- (_ : IsRightCancelMul (Multiplicative α)) = (_ : IsRightCancelMul (Multiplicative α))

## Equations

- (_ : IsCancelAdd (Additive α)) = (_ : IsCancelAdd (Additive α))

## Equations

- (_ : IsCancelMul (Multiplicative α)) = (_ : IsCancelMul (Multiplicative α))

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

- instOneMultiplicative = { one := Multiplicative.ofAdd 0 }

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

- Multiplicative.commMonoid = let src := Multiplicative.monoid; let src_1 := Multiplicative.commSemigroup; CommMonoid.mk (_ : ∀ (a b : Multiplicative α), a * b = b * a)

## Equations

- Multiplicative.inv = { inv := fun (x : Multiplicative α) => Additive.ofMul (-Multiplicative.toAdd x) }

## Equations

- Multiplicative.div = { div := fun (x y : Multiplicative α) => Multiplicative.ofAdd (Multiplicative.toAdd x - Multiplicative.toAdd y) }

## Equations

- Additive.involutiveNeg = let src := Additive.neg; InvolutiveNeg.mk (_ : ∀ (a : α), a⁻¹⁻¹ = a)

## Equations

- Multiplicative.involutiveInv = let src := Multiplicative.inv; InvolutiveInv.mk (_ : ∀ (a : α), - -a = a)

## Equations

- Additive.subNegMonoid = let src := Additive.neg; let src_1 := Additive.sub; let src_2 := Additive.addMonoid; SubNegMonoid.mk DivInvMonoid.zpow

## Equations

- Multiplicative.divInvMonoid = let src := Multiplicative.inv; let src_1 := Multiplicative.div; let src_2 := Multiplicative.monoid; DivInvMonoid.mk SubNegMonoid.zsmul

## Equations

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

## Equations

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

## Equations

- Multiplicative.divisionCommMonoid = let src := Multiplicative.divisionMonoid; let src_1 := Multiplicative.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : Multiplicative α), a * b = b * a)

## Equations

- Multiplicative.commGroup = let src := Multiplicative.group; let src_1 := Multiplicative.commMonoid; CommGroup.mk (_ : ∀ (a b : Multiplicative α), a * b = b * a)

Reinterpret `α →+ β`

as `Multiplicative α →* Multiplicative β`

.

## Equations

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

## Instances For

Reinterpret `α →* β`

as `Additive α →+ Additive β`

.

## Equations

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

## Instances For

Reinterpret `Additive α →+ β`

as `α →* Multiplicative β`

.

## Equations

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

## Instances For

Reinterpret `α →* Multiplicative β`

as `Additive α →+ β`

.

## Equations

- MonoidHom.toAdditive' = AddMonoidHom.toMultiplicative'.symm

## Instances For

Reinterpret `α →+ Additive β`

as `Multiplicative α →* β`

.

## Equations

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

## Instances For

Reinterpret `Multiplicative α →* β`

as `α →+ Additive β`

.

## Equations

- MonoidHom.toAdditive'' = AddMonoidHom.toMultiplicative''.symm

## Instances For

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.coeToFun = { coe := fun (a : Additive α) => CoeFun.coe (Additive.toMul 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.coeToFun = { coe := fun (a : Multiplicative α) => CoeFun.coe (Multiplicative.toAdd a) }