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