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

source

@[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

source

@[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

source

@[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

source

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

source

@[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

source

@[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

source

@[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

source

@[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

source

def MulEquiv.toAdditive {G : Type u_1} {H : Type u_2} [MulOneClass G] [MulOneClass H] :

G ≃* H ≃ (Additive G ≃+ Additive H)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

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

source

@[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.

Equations

MulEquiv.toAdditive' = AddEquiv.toMultiplicative'.symm

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

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

source

@[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.

Equations

MulEquiv.toAdditive'' = AddEquiv.toMultiplicative''.symm

Instances For

source

@[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))

source

@[simp]

theorem monoidEndToAdditive_symm_apply_apply (M : Type u_3) [MulOneClass M] (f : Additive M →+ Additive M) (a : M) :

((MulEquiv.symm (monoidEndToAdditive M)) f) a = Additive.toMul (f (Additive.ofMul a))

source

def monoidEndToAdditive (M : Type u_3) [MulOneClass M] :

Monoid.End M ≃* AddMonoid.End (Additive M)

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

Equations

monoidEndToAdditive M = let __src := MonoidHom.toAdditive; { toEquiv := __src, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem addMonoidEndToMultiplicative_symm_apply_apply (A : Type u_3) [AddZeroClass A] (f : Multiplicative A →* Multiplicative A) (a : A) :

((MulEquiv.symm (addMonoidEndToMultiplicative A)) f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))

source

@[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))

source

def addMonoidEndToMultiplicative (A : Type u_3) [AddZeroClass A] :

AddMonoid.End A ≃* Monoid.End (Multiplicative A)

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

Equations

addMonoidEndToMultiplicative A = let __src := AddMonoidHom.toMultiplicative; { toEquiv := __src, map_mul' := ⋯ }

Instances For

source

@[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)

source

@[simp]

theorem AddEquiv.additiveMultiplicative_apply (G : Type u_1) [AddZeroClass G] (a : Additive (Multiplicative G)) :

(AddEquiv.additiveMultiplicative G) a = Multiplicative.toAdd (Additive.toMul a)

source

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

source

@[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)

source

@[simp]

theorem MulEquiv.multiplicativeAdditive_apply (H : Type u_2) [MulOneClass H] (a : Multiplicative (Additive H)) :

(MulEquiv.multiplicativeAdditive H) a = Additive.toMul (Multiplicative.toAdd a)

source

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))

Instances For

Documentation

Mathlib.Algebra.Group.Equiv.TypeTags

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

Additive and multiplicative equivalences associated to Multiplicative and Additive. #

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