# Documentation

Mathlib.Algebra.Hom.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.

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_apply_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_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.

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'_symm_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : ) (a : ) :
@[simp]
theorem AddEquiv.toMultiplicative'_apply_symm_apply {G : Type u_1} {H : Type u_2} [] [] (f : ≃+ H) (a : ) :
@[simp]
theorem AddEquiv.toMultiplicative'_apply_apply {G : Type u_1} {H : Type u_2} [] [] (f : ≃+ H) (a : G) :
def AddEquiv.toMultiplicative' {G : Type u_1} {H : Type u_2} [] [] :
≃+ H ()

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

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.

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_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 : ) :
def AddEquiv.toMultiplicative'' {G : Type u_1} {H : Type u_2} [] [] :
G ≃+ ()

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

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.

Instances For
@[simp]
@[simp]

Additive (Multiplicative G) is just G.

Instances For
@[simp]
theorem MulEquiv.multiplicativeAdditive_symm_apply (H : Type u_2) [] (a : H) :
Multiplicative (Additive H) is just H.