Additive and multiplicative equivalences associated to Multiplicative
and Additive
. #
@[simp]
theorem
AddEquiv.toMultiplicative_symm_apply_apply
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[AddZeroClass H]
(f : Multiplicative G ≃* Multiplicative H)
(a : G)
:
↑(↑AddEquiv.toMultiplicative.symm f) a = ↑(↑AddMonoidHom.toMultiplicative.symm (MulEquiv.toMonoidHom f)) a
@[simp]
theorem
AddEquiv.toMultiplicative_symm_apply_symm_apply
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[AddZeroClass H]
(f : Multiplicative G ≃* Multiplicative H)
(a : H)
:
↑(AddEquiv.symm (↑AddEquiv.toMultiplicative.symm f)) a = ↑(↑AddMonoidHom.toMultiplicative.symm (MulEquiv.toMonoidHom (MulEquiv.symm f))) a
@[simp]
theorem
AddEquiv.toMultiplicative_apply_symm_apply
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[AddZeroClass H]
(f : G ≃+ H)
(a : Multiplicative H)
:
↑(MulEquiv.symm (↑AddEquiv.toMultiplicative f)) a = ↑(↑AddMonoidHom.toMultiplicative (AddEquiv.toAddMonoidHom (AddEquiv.symm f))) a
@[simp]
theorem
AddEquiv.toMultiplicative_apply_apply
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[AddZeroClass H]
(f : G ≃+ H)
(a : Multiplicative G)
:
↑(↑AddEquiv.toMultiplicative f) a = ↑(↑AddMonoidHom.toMultiplicative (AddEquiv.toAddMonoidHom f)) a
def
AddEquiv.toMultiplicative
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[AddZeroClass H]
:
G ≃+ H ≃ (Multiplicative G ≃* Multiplicative 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}
[MulOneClass G]
[MulOneClass H]
(f : G ≃* H)
(a : Additive H)
:
↑(AddEquiv.symm (↑MulEquiv.toAdditive f)) a = ↑(↑MonoidHom.toAdditive (MulEquiv.toMonoidHom (MulEquiv.symm f))) a
@[simp]
theorem
MulEquiv.toAdditive_apply_apply
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[MulOneClass H]
(f : G ≃* H)
(a : Additive G)
:
↑(↑MulEquiv.toAdditive f) a = ↑(↑MonoidHom.toAdditive (MulEquiv.toMonoidHom f)) a
@[simp]
theorem
MulEquiv.toAdditive_symm_apply_symm_apply
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[MulOneClass H]
(f : Additive G ≃+ Additive H)
(a : H)
:
↑(MulEquiv.symm (↑MulEquiv.toAdditive.symm f)) a = ↑(↑MonoidHom.toAdditive.symm (AddEquiv.toAddMonoidHom (AddEquiv.symm f))) a
@[simp]
theorem
MulEquiv.toAdditive_symm_apply_apply
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[MulOneClass H]
(f : Additive G ≃+ Additive H)
(a : G)
:
↑(↑MulEquiv.toAdditive.symm f) a = ↑(↑MonoidHom.toAdditive.symm (AddEquiv.toAddMonoidHom f)) a
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}
[MulOneClass G]
[AddZeroClass H]
(f : G ≃* Multiplicative H)
(a : H)
:
↑(AddEquiv.symm (↑AddEquiv.toMultiplicative'.symm f)) a = ↑(↑AddMonoidHom.toMultiplicative''.symm (MulEquiv.toMonoidHom (MulEquiv.symm f))) a
@[simp]
theorem
AddEquiv.toMultiplicative'_symm_apply_apply
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[AddZeroClass H]
(f : G ≃* Multiplicative H)
(a : Additive G)
:
↑(↑AddEquiv.toMultiplicative'.symm f) a = ↑(↑AddMonoidHom.toMultiplicative'.symm (MulEquiv.toMonoidHom f)) a
@[simp]
theorem
AddEquiv.toMultiplicative'_apply_symm_apply
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[AddZeroClass H]
(f : Additive G ≃+ H)
(a : Multiplicative H)
:
↑(MulEquiv.symm (↑AddEquiv.toMultiplicative' f)) a = ↑(↑AddMonoidHom.toMultiplicative'' (AddEquiv.toAddMonoidHom (AddEquiv.symm f))) a
@[simp]
theorem
AddEquiv.toMultiplicative'_apply_apply
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[AddZeroClass H]
(f : Additive G ≃+ H)
(a : G)
:
↑(↑AddEquiv.toMultiplicative' f) a = ↑(↑AddMonoidHom.toMultiplicative' (AddEquiv.toAddMonoidHom f)) a
def
AddEquiv.toMultiplicative'
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[AddZeroClass H]
:
Additive G ≃+ H ≃ (G ≃* Multiplicative H)
Reinterpret Additive G ≃+ H
as G ≃* Multiplicative H
.
Instances For
@[inline, reducible]
abbrev
MulEquiv.toAdditive'
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[AddZeroClass H]
:
G ≃* Multiplicative H ≃ (Additive G ≃+ 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}
[AddZeroClass G]
[MulOneClass H]
(f : G ≃+ Additive H)
(a : Multiplicative G)
:
↑(↑AddEquiv.toMultiplicative'' f) a = ↑(↑AddMonoidHom.toMultiplicative'' (AddEquiv.toAddMonoidHom f)) a
@[simp]
theorem
AddEquiv.toMultiplicative''_apply_symm_apply
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[MulOneClass H]
(f : G ≃+ Additive H)
(a : H)
:
↑(MulEquiv.symm (↑AddEquiv.toMultiplicative'' f)) a = ↑(↑AddMonoidHom.toMultiplicative' (AddEquiv.toAddMonoidHom (AddEquiv.symm f))) a
@[simp]
theorem
AddEquiv.toMultiplicative''_symm_apply_apply
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[MulOneClass H]
(f : Multiplicative G ≃* H)
(a : G)
:
↑(↑AddEquiv.toMultiplicative''.symm f) a = ↑(↑AddMonoidHom.toMultiplicative''.symm (MulEquiv.toMonoidHom f)) a
@[simp]
theorem
AddEquiv.toMultiplicative''_symm_apply_symm_apply
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[MulOneClass H]
(f : Multiplicative G ≃* H)
(a : Additive H)
:
↑(AddEquiv.symm (↑AddEquiv.toMultiplicative''.symm f)) a = ↑(↑AddMonoidHom.toMultiplicative'.symm (MulEquiv.toMonoidHom (MulEquiv.symm f))) a
def
AddEquiv.toMultiplicative''
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[MulOneClass H]
:
G ≃+ Additive H ≃ (Multiplicative G ≃* H)
Reinterpret G ≃+ Additive H
as Multiplicative G ≃* H
.
Instances For
@[inline, reducible]
abbrev
MulEquiv.toAdditive''
{G : Type u_1}
{H : Type u_2}
[AddZeroClass G]
[MulOneClass H]
:
Multiplicative G ≃* H ≃ (G ≃+ Additive H)
Reinterpret Multiplicative G ≃* H
as G ≃+ Additive H
as.
Instances For
@[simp]
theorem
AddEquiv.additiveMultiplicative_symm_apply
(G : Type u_1)
[AddZeroClass G]
(a : G)
:
↑(AddEquiv.symm (AddEquiv.additiveMultiplicative G)) a = ↑Additive.ofMul (↑Multiplicative.ofAdd a)
@[simp]
theorem
AddEquiv.additiveMultiplicative_apply
(G : Type u_1)
[AddZeroClass G]
(a : Additive (Multiplicative G))
:
↑(AddEquiv.additiveMultiplicative G) a = ↑Multiplicative.toAdd (↑Additive.toMul a)
def
AddEquiv.additiveMultiplicative
(G : Type u_1)
[AddZeroClass G]
:
Additive (Multiplicative G) ≃+ G
Additive (Multiplicative G)
is just G
.
Instances For
@[simp]
theorem
MulEquiv.multiplicativeAdditive_symm_apply
(H : Type u_2)
[MulOneClass H]
(a : H)
:
↑(MulEquiv.symm (MulEquiv.multiplicativeAdditive H)) a = ↑Multiplicative.ofAdd (↑Additive.ofMul a)
@[simp]
theorem
MulEquiv.multiplicativeAdditive_apply
(H : Type u_2)
[MulOneClass H]
(a : Multiplicative (Additive H))
:
↑(MulEquiv.multiplicativeAdditive H) a = ↑Additive.toMul (↑Multiplicative.toAdd a)
def
MulEquiv.multiplicativeAdditive
(H : Type u_2)
[MulOneClass H]
:
Multiplicative (Additive H) ≃* H
Multiplicative (Additive H)
is just H
.