Additive and multiplicative equivalences associated to Multiplicative
and Additive
. #
@[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.toMultiplicative.symm f).symm a = (AddMonoidHom.toMultiplicative.symm f.symm.toMonoidHom) 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)
:
(AddEquiv.toMultiplicative f).symm a = (AddMonoidHom.toMultiplicative f.symm.toAddMonoidHom) a
@[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 f.toMonoidHom) 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 f.toAddMonoidHom) 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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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.toAdditive.symm f).symm a = (MonoidHom.toAdditive.symm f.symm.toAddMonoidHom) a
@[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)
:
(MulEquiv.toAdditive f).symm a = (MonoidHom.toAdditive f.symm.toMonoidHom) 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 f.toMonoidHom) 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 f.toAddMonoidHom) a
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'_apply_symm_apply
{G : Type u_1}
{H : Type u_2}
[MulOneClass G]
[AddZeroClass H]
(f : Additive G ≃+ H)
(a : Multiplicative H)
:
(AddEquiv.toMultiplicative' f).symm a = (AddMonoidHom.toMultiplicative'' f.symm.toAddMonoidHom) a
@[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.toMultiplicative'.symm f).symm a = (AddMonoidHom.toMultiplicative''.symm f.symm.toMonoidHom) 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' f.toAddMonoidHom) 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 f.toMonoidHom) 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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
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.
Equations
- MulEquiv.toAdditive' = AddEquiv.toMultiplicative'.symm
Instances For
@[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 f.toMonoidHom) a
@[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'' f.toAddMonoidHom) 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.toMultiplicative''.symm f).symm a = (AddMonoidHom.toMultiplicative'.symm f.symm.toMonoidHom) 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)
:
(AddEquiv.toMultiplicative'' f).symm a = (AddMonoidHom.toMultiplicative' f.symm.toAddMonoidHom) 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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
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.
Equations
- MulEquiv.toAdditive'' = AddEquiv.toMultiplicative''.symm
Instances For
@[simp]
theorem
monoidEndToAdditive_symm_apply_apply
(M : Type u_3)
[MulOneClass M]
(f : Additive M →+ Additive M)
(a : M)
:
((monoidEndToAdditive M).symm f) a = Additive.toMul (f (Additive.ofMul a))
@[simp]
theorem
monoidEndToAdditive_apply_apply
(M : Type u_3)
[MulOneClass M]
(f : M →* M)
(a : Additive M)
:
((monoidEndToAdditive M) f) a = Additive.ofMul (f (Additive.toMul a))
Multiplicative equivalence between multiplicative endomorphisms of a MulOneClass
M
and additive endomorphisms of Additive M
.
Equations
- monoidEndToAdditive M = { toEquiv := MonoidHom.toAdditive, map_mul' := ⋯ }
Instances For
@[simp]
theorem
addMonoidEndToMultiplicative_symm_apply_apply
(A : Type u_3)
[AddZeroClass A]
(f : Multiplicative A →* Multiplicative A)
(a : A)
:
((addMonoidEndToMultiplicative A).symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))
@[simp]
theorem
addMonoidEndToMultiplicative_apply_apply
(A : Type u_3)
[AddZeroClass A]
(f : A →+ A)
(a : Multiplicative A)
:
((addMonoidEndToMultiplicative A) f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))
Multiplicative equivalence between additive endomorphisms of an AddZeroClass
A
and multiplicative endomorphisms of Multiplicative A
.
Equations
- addMonoidEndToMultiplicative A = { toEquiv := AddMonoidHom.toMultiplicative, map_mul' := ⋯ }
Instances For
@[simp]
theorem
AddEquiv.additiveMultiplicative_symm_apply
(G : Type u_1)
[AddZeroClass G]
(a : G)
:
(AddEquiv.additiveMultiplicative G).symm 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
.
Equations
- AddEquiv.additiveMultiplicative G = MulEquiv.toAdditive' (MulEquiv.refl (Multiplicative G))
Instances For
@[simp]
theorem
MulEquiv.multiplicativeAdditive_apply
(H : Type u_2)
[MulOneClass H]
(a : Multiplicative (Additive H))
:
(MulEquiv.multiplicativeAdditive H) a = Additive.toMul (Multiplicative.toAdd a)
@[simp]
theorem
MulEquiv.multiplicativeAdditive_symm_apply
(H : Type u_2)
[MulOneClass H]
(a : H)
:
(MulEquiv.multiplicativeAdditive H).symm a = Multiplicative.ofAdd (Additive.ofMul a)
def
MulEquiv.multiplicativeAdditive
(H : Type u_2)
[MulOneClass H]
:
Multiplicative (Additive H) ≃* H
Multiplicative (Additive H)
is just H
.
Equations
- MulEquiv.multiplicativeAdditive H = AddEquiv.toMultiplicative'' (AddEquiv.refl (Additive H))