Documentation

Mathlib.Algebra.Hom.Equiv.TypeTags

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] :

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] :

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] :

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] :

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] :

Reinterpret Multiplicative G ≃* H≃* H as G ≃+ Additive H≃+ Additive H as.

Equations
  • MulEquiv.toAdditive'' = Equiv.symm AddEquiv.toMultiplicative''

Additive (Multiplicative G) is just G.

Equations

Multiplicative (Additive H) is just H.

Equations