Documentation

Mathlib.Algebra.Hom.Equiv.TypeTags

Additive and multiplicative equivalences associated to Multiplicative and Additive. #

source
ink
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.
source
ink
def MulEquiv.toAdditive {G : Type u_1} {H : Type u_2} [inst : MulOneClass G] [inst : MulOneClass H] :
G ≃* H ≃ (Additive G ≃+ Additive 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.
source
ink
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.
source
ink
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'
source
ink
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.
source
ink
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''
source
ink
def AddEquiv.additiveMultiplicative (G : Type u_1) [inst : AddZeroClass G] :
Additive (Multiplicative G) ≃+ G

Additive (Multiplicative G) is just G.

Equations
source
ink
def MulEquiv.multiplicativeAdditive (H : Type u_1) [inst : MulOneClass H] :
Multiplicative (Additive H) ≃* H

Multiplicative (Additive H) is just H.

Equations