Additive and multiplicative equivalences associated to Multiplicative and Additive.

def AddEquiv.toMultiplicative {G : Type u_2} {H : Type u_3} [Add G] [Add 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.

@[simp]

theorem AddEquiv.toMultiplicative_apply_apply {G : Type u_2} {H : Type u_3} [Add G] [Add H] (f : G ≃+ H) (x : Multiplicative G) : (toMultiplicative f) x = Multiplicative.ofAdd (f (Multiplicative.toAdd x))

@[simp]

theorem AddEquiv.toMultiplicative_symm_apply_apply {G : Type u_2} {H : Type u_3} [Add G] [Add H] (f : Multiplicative G ≃* Multiplicative H) (x : G) : (toMultiplicative.symm f) x = Multiplicative.toAdd (f (Multiplicative.ofAdd x))

@[simp]

theorem AddEquiv.toMultiplicative_symm_apply_symm_apply {G : Type u_2} {H : Type u_3} [Add G] [Add H] (f : Multiplicative G ≃* Multiplicative H) (x : H) : (toMultiplicative.symm f).symm x = Multiplicative.toAdd (f.symm (Multiplicative.ofAdd x))

@[simp]

theorem AddEquiv.toMultiplicative_apply_symm_apply {G : Type u_2} {H : Type u_3} [Add G] [Add H] (f : G ≃+ H) (x : Multiplicative H) : (toMultiplicative f).symm x = Multiplicative.ofAdd (f.symm (Multiplicative.toAdd x))

def MulEquiv.toAdditive {G : Type u_2} {H : Type u_3} [Mul G] [Mul 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.

@[simp]

theorem MulEquiv.toAdditive_apply_symm_apply {G : Type u_2} {H : Type u_3} [Mul G] [Mul H] (f : G ≃* H) (x : Additive H) : (toAdditive f).symm x = Additive.ofMul (f.symm (Additive.toMul x))

@[simp]

theorem MulEquiv.toAdditive_symm_apply_apply {G : Type u_2} {H : Type u_3} [Mul G] [Mul H] (f : Additive G ≃+ Additive H) (x : G) : (toAdditive.symm f) x = Additive.toMul (f (Additive.ofMul x))

@[simp]

theorem MulEquiv.toAdditive_symm_apply_symm_apply {G : Type u_2} {H : Type u_3} [Mul G] [Mul H] (f : Additive G ≃+ Additive H) (x : H) : (toAdditive.symm f).symm x = Additive.toMul (f.symm (Additive.ofMul x))

@[simp]

theorem MulEquiv.toAdditive_apply_apply {G : Type u_2} {H : Type u_3} [Mul G] [Mul H] (f : G ≃* H) (x : Additive G) : (toAdditive f) x = Additive.ofMul (f (Additive.toMul x))

def AddEquiv.toMultiplicativeRight {G : Type u_2} {H : Type u_3} [Mul G] [Add 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.

@[simp]

theorem AddEquiv.toMultiplicativeRight_symm_apply_apply {G : Type u_2} {H : Type u_3} [Mul G] [Add H] (f : G ≃* Multiplicative H) (x : Additive G) : (toMultiplicativeRight.symm f) x = Multiplicative.toAdd (f (Additive.toMul x))

@[simp]

theorem AddEquiv.toMultiplicativeRight_symm_apply_symm_apply {G : Type u_2} {H : Type u_3} [Mul G] [Add H] (f : G ≃* Multiplicative H) (x : H) : (toMultiplicativeRight.symm f).symm x = Additive.ofMul (f.symm (Multiplicative.ofAdd x))

@[simp]

theorem AddEquiv.toMultiplicativeRight_apply_apply {G : Type u_2} {H : Type u_3} [Mul G] [Add H] (f : Additive G ≃+ H) (x : G) : (toMultiplicativeRight f) x = Multiplicative.ofAdd (f (Additive.ofMul x))

@[simp]

theorem AddEquiv.toMultiplicativeRight_apply_symm_apply {G : Type u_2} {H : Type u_3} [Mul G] [Add H] (f : Additive G ≃+ H) (x : Multiplicative H) : (toMultiplicativeRight f).symm x = Additive.toMul (f.symm (Multiplicative.toAdd x))

@[reducible, inline]

abbrev MulEquiv.toAdditiveLeft {G : Type u_2} {H : Type u_3} [Mul G] [Add H] : G ≃* Multiplicative H ≃ (Additive G ≃+ H)

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

Equations

• MulEquiv.toAdditiveLeft = AddEquiv.toMultiplicativeRight.symm

def AddEquiv.toMultiplicativeLeft {G : Type u_2} {H : Type u_3} [Add G] [Mul 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.

@[simp]

theorem AddEquiv.toMultiplicativeLeft_apply_apply {G : Type u_2} {H : Type u_3} [Add G] [Mul H] (f : G ≃+ Additive H) (x : Multiplicative G) : (toMultiplicativeLeft f) x = Additive.toMul (f (Multiplicative.toAdd x))

@[simp]

theorem AddEquiv.toMultiplicativeLeft_symm_apply_apply {G : Type u_2} {H : Type u_3} [Add G] [Mul H] (f : Multiplicative G ≃* H) (x : G) : (toMultiplicativeLeft.symm f) x = Additive.ofMul (f (Multiplicative.ofAdd x))

@[simp]

theorem AddEquiv.toMultiplicativeLeft_apply_symm_apply {G : Type u_2} {H : Type u_3} [Add G] [Mul H] (f : G ≃+ Additive H) (x : H) : (toMultiplicativeLeft f).symm x = Multiplicative.ofAdd (f.symm (Additive.ofMul x))

@[simp]

theorem AddEquiv.toMultiplicativeLeft_symm_apply_symm_apply {G : Type u_2} {H : Type u_3} [Add G] [Mul H] (f : Multiplicative G ≃* H) (x : Additive H) : (toMultiplicativeLeft.symm f).symm x = Multiplicative.toAdd (f.symm (Additive.toMul x))

@[reducible, inline]

abbrev MulEquiv.toAdditiveRight {G : Type u_2} {H : Type u_3} [Add G] [Mul H] : Multiplicative G ≃* H ≃ (G ≃+ Additive H)

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

Equations

• MulEquiv.toAdditiveRight = AddEquiv.toMultiplicativeLeft.symm

def MulEquiv.monoidEnd (M : Type u_4) [MulOneClass M] : _root_.Monoid.End M ≃* _root_.AddMonoid.End (Additive M)

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

Equations

• MulEquiv.monoidEnd M = { toEquiv := MonoidHom.toAdditive, map_mul' := ⋯ }

@[simp]

theorem MulEquiv.monoidEnd_apply_apply (M : Type u_4) [MulOneClass M] (f : M →* M) (a : Additive M) : ((monoidEnd M) f) a = Additive.ofMul (f (Additive.toMul a))

@[simp]

theorem MulEquiv.monoidEnd_symm_apply_apply (M : Type u_4) [MulOneClass M] (f : Additive M →+ Additive M) (a : M) : ((monoidEnd M).symm f) a = Additive.toMul (f (Additive.ofMul a))

def MulEquiv.addMonoidEnd (A : Type u_4) [AddZeroClass A] : _root_.AddMonoid.End A ≃* _root_.Monoid.End (Multiplicative A)

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

Equations

• MulEquiv.addMonoidEnd A = { toEquiv := AddMonoidHom.toMultiplicative, map_mul' := ⋯ }

@[simp]

theorem MulEquiv.addMonoidEnd_apply_apply (A : Type u_4) [AddZeroClass A] (f : A →+ A) (a : Multiplicative A) : ((addMonoidEnd A) f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))

@[simp]

theorem MulEquiv.addMonoidEnd_symm_apply_apply (A : Type u_4) [AddZeroClass A] (f : Multiplicative A →* Multiplicative A) (a : A) : ((addMonoidEnd A).symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))

@[deprecated MulEquiv.monoidEnd (since := "2026-09-10")]

def monoidEndToAdditive (M : Type u_4) [MulOneClass M] : Monoid.End M ≃* AddMonoid.End (Additive M)

Alias of MulEquiv.monoidEnd.

---

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

Equations

• monoidEndToAdditive = MulEquiv.monoidEnd

@[deprecated MulEquiv.monoidEnd_apply_apply (since := "2026-09-10")]

theorem monoidEndToAdditive_apply_apply (M : Type u_4) [MulOneClass M] (f : M →* M) (a : Additive M) : ((MulEquiv.monoidEnd M) f) a = Additive.ofMul (f (Additive.toMul a))

Alias of MulEquiv.monoidEnd_apply_apply.

@[deprecated MulEquiv.monoidEnd_symm_apply_apply (since := "2026-09-10")]

theorem monoidEndToAdditive_symm_apply_apply (M : Type u_4) [MulOneClass M] (f : Additive M →+ Additive M) (a : M) : ((MulEquiv.monoidEnd M).symm f) a = Additive.toMul (f (Additive.ofMul a))

Alias of MulEquiv.monoidEnd_symm_apply_apply.

@[deprecated MulEquiv.addMonoidEnd (since := "2026-09-10")]

def addMonoidEndToMultiplicative (A : Type u_4) [AddZeroClass A] : AddMonoid.End A ≃* Monoid.End (Multiplicative A)

Alias of MulEquiv.addMonoidEnd.

---

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

Equations

• addMonoidEndToMultiplicative = MulEquiv.addMonoidEnd

@[deprecated MulEquiv.addMonoidEnd_apply_apply (since := "2026-09-10")]

theorem addMonoidEndToMultiplicative_apply_apply (A : Type u_4) [AddZeroClass A] (f : A →+ A) (a : Multiplicative A) : ((MulEquiv.addMonoidEnd A) f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))

Alias of MulEquiv.addMonoidEnd_apply_apply.

@[deprecated MulEquiv.addMonoidEnd_symm_apply_apply (since := "2026-09-10")]

theorem addMonoidEndToMultiplicative_symm_apply_apply (A : Type u_4) [AddZeroClass A] (f : Multiplicative A →* Multiplicative A) (a : A) : ((MulEquiv.addMonoidEnd A).symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))

Alias of MulEquiv.addMonoidEnd_symm_apply_apply.

@[deprecated MulEquiv.monoidEnd (since := "2026-09-10")]

def MulEquiv.Monoid.End (M : Type u_4) [MulOneClass M] : _root_.Monoid.End M ≃* _root_.AddMonoid.End (Additive M)

Alias of MulEquiv.monoidEnd.

---

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

Equations

• MulEquiv.Monoid.End = MulEquiv.monoidEnd

@[deprecated MulEquiv.monoidEnd_apply_apply (since := "2026-09-10")]

theorem MulEquiv.Monoid.End_apply_apply (M : Type u_4) [MulOneClass M] (f : M →* M) (a : Additive M) : ((monoidEnd M) f) a = Additive.ofMul (f (Additive.toMul a))

Alias of MulEquiv.monoidEnd_apply_apply.

@[deprecated MulEquiv.monoidEnd_symm_apply_apply (since := "2026-09-10")]

theorem MulEquiv.Monoid.End_symm_apply_apply (M : Type u_4) [MulOneClass M] (f : Additive M →+ Additive M) (a : M) : ((monoidEnd M).symm f) a = Additive.toMul (f (Additive.ofMul a))

Alias of MulEquiv.monoidEnd_symm_apply_apply.

@[deprecated MulEquiv.addMonoidEnd (since := "2026-09-10")]

def MulEquiv.AddMonoid.End (A : Type u_4) [AddZeroClass A] : _root_.AddMonoid.End A ≃* _root_.Monoid.End (Multiplicative A)

Alias of MulEquiv.addMonoidEnd.

---

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

Equations

• MulEquiv.AddMonoid.End = MulEquiv.addMonoidEnd

@[deprecated MulEquiv.addMonoidEnd_apply_apply (since := "2026-09-10")]

theorem MulEquiv.AddMonoid.End_apply_apply (A : Type u_4) [AddZeroClass A] (f : A →+ A) (a : Multiplicative A) : ((addMonoidEnd A) f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))

Alias of MulEquiv.addMonoidEnd_apply_apply.

@[deprecated MulEquiv.addMonoidEnd_symm_apply_apply (since := "2026-09-10")]

theorem MulEquiv.AddMonoid.End_symm_apply_apply (A : Type u_4) [AddZeroClass A] (f : Multiplicative A →* Multiplicative A) (a : A) : ((addMonoidEnd A).symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))

Alias of MulEquiv.addMonoidEnd_symm_apply_apply.

def MulEquiv.piMultiplicative {ι : Type u_1} (K : ι → Type u_4) [(i : ι) → Add (K i)] : Multiplicative ((i : ι) → K i) ≃* ((i : ι) → Multiplicative (K i))

Multiplicative (∀ i : ι, K i) is equivalent to ∀ i : ι, Multiplicative (K i).

Equations

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

@[simp]

theorem MulEquiv.piMultiplicative_symm_apply {ι : Type u_1} (K : ι → Type u_4) [(i : ι) → Add (K i)] (x : (i : ι) → Multiplicative (K i)) : (piMultiplicative K).symm x = Multiplicative.ofAdd fun (i : ι) => Multiplicative.toAdd (x i)

@[simp]

theorem MulEquiv.piMultiplicative_apply {ι : Type u_1} (K : ι → Type u_4) [(i : ι) → Add (K i)] (x : Multiplicative ((i : ι) → K i)) (i : ι) : (piMultiplicative K) x i = Multiplicative.ofAdd (Multiplicative.toAdd x i)

@[reducible, inline]

abbrev MulEquiv.funMultiplicative (ι : Type u_1) (G : Type u_2) [Add G] : Multiplicative (ι → G) ≃* (ι → Multiplicative G)

Multiplicative (ι → G) is equivalent to ι → Multiplicative G.

Equations

• MulEquiv.funMultiplicative ι G = MulEquiv.piMultiplicative fun (x : ι) => G

def AddEquiv.piAdditive {ι : Type u_1} (K : ι → Type u_4) [(i : ι) → Mul (K i)] : Additive ((i : ι) → K i) ≃+ ((i : ι) → Additive (K i))

Additive (∀ i : ι, K i) is equivalent to ∀ i : ι, Additive (K i).

Equations

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

@[simp]

theorem AddEquiv.piAdditive_symm_apply {ι : Type u_1} (K : ι → Type u_4) [(i : ι) → Mul (K i)] (x : (i : ι) → Additive (K i)) : (piAdditive K).symm x = Additive.ofMul fun (i : ι) => Additive.toMul (x i)

@[simp]

theorem AddEquiv.piAdditive_apply {ι : Type u_1} (K : ι → Type u_4) [(i : ι) → Mul (K i)] (x : Additive ((i : ι) → K i)) (i : ι) : (piAdditive K) x i = Additive.ofMul (Additive.toMul x i)

@[reducible, inline]

abbrev AddEquiv.funAdditive (ι : Type u_1) (G : Type u_2) [Mul G] : Additive (ι → G) ≃+ (ι → Additive G)

Additive (ι → G) is equivalent to ι → Additive G.

Equations

• AddEquiv.funAdditive ι G = AddEquiv.piAdditive fun (x : ι) => G

def AddEquiv.additiveMultiplicative (G : Type u_2) [Add G] : Additive (Multiplicative G) ≃+ G

Additive (Multiplicative G) is just G.

Equations

• AddEquiv.additiveMultiplicative G = MulEquiv.toAdditiveLeft (MulEquiv.refl (Multiplicative G))

@[simp]

theorem AddEquiv.additiveMultiplicative_symm_apply (G : Type u_2) [Add G] (x : G) : (additiveMultiplicative G).symm x = Additive.ofMul (Multiplicative.ofAdd x)

@[simp]

theorem AddEquiv.additiveMultiplicative_apply (G : Type u_2) [Add G] (x : Additive (Multiplicative G)) : (additiveMultiplicative G) x = Multiplicative.toAdd (Additive.toMul x)

def MulEquiv.multiplicativeAdditive (H : Type u_3) [Mul H] : Multiplicative (Additive H) ≃* H

Multiplicative (Additive H) is just H.

Equations

• MulEquiv.multiplicativeAdditive H = AddEquiv.toMultiplicativeLeft (AddEquiv.refl (Additive H))

@[simp]

theorem MulEquiv.multiplicativeAdditive_symm_apply (H : Type u_3) [Mul H] (x : H) : (multiplicativeAdditive H).symm x = Multiplicative.ofAdd (Additive.ofMul x)

@[simp]

theorem MulEquiv.multiplicativeAdditive_apply (H : Type u_3) [Mul H] (x : Multiplicative (Additive H)) : (multiplicativeAdditive H) x = Additive.toMul (Multiplicative.toAdd x)

@[deprecated MulEquiv.multiplicativeAdditive (since := "2026-09-10")]

def MulEquiv.toMultiplicative_toAdditive (H : Type u_3) [Mul H] : Multiplicative (Additive H) ≃* H

Alias of MulEquiv.multiplicativeAdditive.

---

Multiplicative (Additive H) is just H.

Equations

• MulEquiv.toMultiplicative_toAdditive = MulEquiv.multiplicativeAdditive

@[deprecated MulEquiv.multiplicativeAdditive_apply (since := "2026-09-10")]

theorem MulEquiv.toMultiplicative_toAdditive_apply (H : Type u_3) [Mul H] (x : Multiplicative (Additive H)) : (multiplicativeAdditive H) x = Additive.toMul (Multiplicative.toAdd x)

Alias of MulEquiv.multiplicativeAdditive_apply.

@[deprecated MulEquiv.multiplicativeAdditive_symm_apply (since := "2026-09-10")]

theorem MulEquiv.toMultiplicative_toAdditive_symm_apply (H : Type u_3) [Mul H] (x : H) : (multiplicativeAdditive H).symm x = Multiplicative.ofAdd (Additive.ofMul x)

Alias of MulEquiv.multiplicativeAdditive_symm_apply.

@[deprecated AddEquiv.additiveMultiplicative (since := "2026-09-10")]

def AddEquiv.toAdditive_toMultiplicative (G : Type u_2) [Add G] : Additive (Multiplicative G) ≃+ G

Alias of AddEquiv.additiveMultiplicative.

---

Additive (Multiplicative G) is just G.

Equations

• AddEquiv.toAdditive_toMultiplicative = AddEquiv.additiveMultiplicative

@[deprecated AddEquiv.additiveMultiplicative_apply (since := "2026-09-10")]

theorem AddEquiv.toAdditive_toMultiplicative_apply (G : Type u_2) [Add G] (x : Additive (Multiplicative G)) : (additiveMultiplicative G) x = Multiplicative.toAdd (Additive.toMul x)

Alias of AddEquiv.additiveMultiplicative_apply.

@[deprecated AddEquiv.additiveMultiplicative_symm_apply (since := "2026-09-10")]

theorem AddEquiv.toAdditive_toMultiplicative_symm_apply (G : Type u_2) [Add G] (x : G) : (additiveMultiplicative G).symm x = Additive.ofMul (Multiplicative.ofAdd x)

Alias of AddEquiv.additiveMultiplicative_symm_apply.

def MulEquiv.prodMultiplicative (G : Type u_2) (H : Type u_3) [Add G] [Add H] : Multiplicative (G × H) ≃* Multiplicative G × Multiplicative H

Multiplicative (G × H) is equivalent to Multiplicative G × Multiplicative H.

Equations

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

@[simp]

theorem MulEquiv.prodMultiplicative_symm_apply (G : Type u_2) (H : Type u_3) [Add G] [Add H] (x✝ : Multiplicative G × Multiplicative H) : (prodMultiplicative G H).symm x✝ = match x✝ with | (x, y) => Multiplicative.ofAdd (Multiplicative.toAdd x, Multiplicative.toAdd y)

@[simp]

theorem MulEquiv.prodMultiplicative_apply (G : Type u_2) (H : Type u_3) [Add G] [Add H] (x : Multiplicative (G × H)) : (prodMultiplicative G H) x = (Multiplicative.ofAdd (Multiplicative.toAdd x).1, Multiplicative.ofAdd (Multiplicative.toAdd x).2)

def AddEquiv.prodAdditive (G : Type u_2) (H : Type u_3) [Mul G] [Mul H] : Additive (G × H) ≃+ Additive G × Additive H

Additive (G × H) is equivalent to Additive G × Additive H.

Equations

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

@[simp]

theorem AddEquiv.prodAdditive_apply (G : Type u_2) (H : Type u_3) [Mul G] [Mul H] (x : Additive (G × H)) : (prodAdditive G H) x = (Additive.ofMul (Additive.toMul x).1, Additive.ofMul (Additive.toMul x).2)

@[simp]

theorem AddEquiv.prodAdditive_symm_apply (G : Type u_2) (H : Type u_3) [Mul G] [Mul H] (x✝ : Additive G × Additive H) : (prodAdditive G H).symm x✝ = match x✝ with | (x, y) => Additive.ofMul (Additive.toMul x, Additive.toMul y)