# Documentation

Mathlib.Algebra.Group.Equiv.TypeTags

# Additive and multiplicative equivalences associated to Multiplicative and Additive. #

@[simp]
theorem AddEquiv.toMultiplicative_symm_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : G) :
@[simp]
theorem AddEquiv.toMultiplicative_symm_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : H) :
@[simp]
theorem AddEquiv.toMultiplicative_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : G ≃+ H) (a : ) :
@[simp]
theorem AddEquiv.toMultiplicative_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : G ≃+ H) (a : ) :
def AddEquiv.toMultiplicative {G : Type u_1} {H : Type u_2} [] [] :
G ≃+ H ()

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MulEquiv.toAdditive_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : G ≃* H) (a : ) :
@[simp]
theorem MulEquiv.toAdditive_symm_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : H) :
@[simp]
theorem MulEquiv.toAdditive_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : G ≃* H) (a : ) :
@[simp]
theorem MulEquiv.toAdditive_symm_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : G) :
def MulEquiv.toAdditive {G : Type u_1} {H : Type u_2} [] [] :
G ≃* H ()

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddEquiv.toMultiplicative'_symm_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : H) :
@[simp]
theorem AddEquiv.toMultiplicative'_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : ≃+ H) (a : G) :
@[simp]
theorem AddEquiv.toMultiplicative'_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : ≃+ H) (a : ) :
@[simp]
theorem AddEquiv.toMultiplicative'_symm_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : ) :
def AddEquiv.toMultiplicative' {G : Type u_1} {H : Type u_2} [] [] :
≃+ H ()

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline, reducible]
abbrev MulEquiv.toAdditive' {G : Type u_1} {H : Type u_2} [] [] :
( ≃+ H)

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

Equations
Instances For
@[simp]
theorem AddEquiv.toMultiplicative''_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : G ≃+ ) (a : ) :
@[simp]
theorem AddEquiv.toMultiplicative''_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : G ≃+ ) (a : H) :
@[simp]
theorem AddEquiv.toMultiplicative''_symm_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : ) :
@[simp]
theorem AddEquiv.toMultiplicative''_symm_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : G) :
def AddEquiv.toMultiplicative'' {G : Type u_1} {H : Type u_2} [] [] :
G ≃+ ()

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline, reducible]
abbrev MulEquiv.toAdditive'' {G : Type u_1} {H : Type u_2} [] [] :
(G ≃+ )

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

Equations
Instances For
@[simp]
theorem monoidEndToAdditive_apply (M : Type u_3) [] :
∀ (a : M →* M), a = Equiv.toFun MonoidHom.toAdditive a
@[simp]
theorem monoidEndToAdditive_symm_apply (M : Type u_3) [] :
∀ (a : ), a = Equiv.invFun MonoidHom.toAdditive a
def monoidEndToAdditive (M : Type u_3) [] :

Multiplicative equivalence between multiplicative endomorphisms of a MulOneClass M and additive endomorphisms of Additive M.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem addMonoidEndToMultiplicative_symm_apply (A : Type u_3) [] :
∀ (a : ), = Equiv.invFun AddMonoidHom.toMultiplicative a
@[simp]
theorem addMonoidEndToMultiplicative_apply (A : Type u_3) [] :
∀ (a : A →+ A), = Equiv.toFun AddMonoidHom.toMultiplicative a

Multiplicative equivalence between additive endomorphisms of an AddZeroClass A and multiplicative endomorphisms of Multiplicative A.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]

Additive (Multiplicative G) is just G.

Equations
Multiplicative (Additive H) is just H.