Type tags that turn additive structures into multiplicative, and vice versa

We define two type tags:

• Additive α: turns any multiplicative structure on α into the corresponding additive structure on Additive α;
• Multiplicative α: turns any additive structure on α into the corresponding multiplicative structure on Multiplicative α.

We also define instances Additive.* and Multiplicative.* that actually transfer the structures.

See also

This file is similar to Order.Synonym.

Porting notes

• Since bundled morphism applications that rely on CoeFun currently don't work, they are ported as toFoo a rather than a.toFoo for now. (https://github.com/leanprover/lean4/issues/1910)

ink

def Additive (α : Type u_1) : Type u_1

If α carries some multiplicative structure, then Additive α carries the corresponding additive structure.

Equations

• Additive α = α

ink

def Multiplicative (α : Type u_1) : Type u_1

If α carries some additive structure, then Multiplicative α carries the corresponding multiplicative structure.

Equations

• Multiplicative α = α

ink

def Additive.ofMul {α : Type u} : α ≃ Additive α

Reinterpret x : α as an element of Additive α.

Equations

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

ink

def Additive.toMul {α : Type u} : Additive α ≃ α

Reinterpret x : Additive α as an element of α.

Equations

• Additive.toMul = Equiv.symm Additive.ofMul

ink

@[simp]

theorem Additive.ofMul_symm_eq {α : Type u} : Equiv.symm Additive.ofMul = Additive.toMul

ink

@[simp]

theorem Additive.toMul_symm_eq {α : Type u} : Equiv.symm Additive.toMul = Additive.ofMul

ink

def Multiplicative.ofAdd {α : Type u} : α ≃ Multiplicative α

Reinterpret x : α as an element of Multiplicative α.

Equations

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

ink

def Multiplicative.toAdd {α : Type u} : Multiplicative α ≃ α

Reinterpret x : Multiplicative α as an element of α.

Equations

• Multiplicative.toAdd = Equiv.symm Multiplicative.ofAdd

ink

@[simp]

theorem Multiplicative.ofAdd_symm_eq {α : Type u} : Equiv.symm Multiplicative.ofAdd = Multiplicative.toAdd

ink

@[simp]

theorem Multiplicative.toAdd_symm_eq {α : Type u} : Equiv.symm Multiplicative.toAdd = Multiplicative.ofAdd

ink

@[simp]

theorem toAdd_ofAdd {α : Type u} (x : α) : ↑Multiplicative.toAdd (↑Multiplicative.ofAdd x) = x

ink

@[simp]

theorem ofAdd_toAdd {α : Type u} (x : Multiplicative α) : ↑Multiplicative.ofAdd (↑Multiplicative.toAdd x) = x

ink

@[simp]

theorem toMul_ofMul {α : Type u} (x : α) : ↑Additive.toMul (↑Additive.ofMul x) = x

ink

@[simp]

theorem ofMul_toMul {α : Type u} (x : Additive α) : ↑Additive.ofMul (↑Additive.toMul x) = x

ink

instance instInhabitedAdditive {α : Type u} [inst : Inhabited α] : Inhabited (Additive α)

Equations

• instInhabitedAdditive = { default := ↑Additive.ofMul default }

ink

instance instInhabitedMultiplicative {α : Type u} [inst : Inhabited α] : Inhabited (Multiplicative α)

Equations

• instInhabitedMultiplicative = { default := ↑Multiplicative.ofAdd default }

ink

instance instFiniteAdditive {α : Type u} [inst : Finite α] : Finite (Additive α)

Equations

• @instFiniteAdditive = @instFiniteAdditive.proof_1

ink

instance instFiniteMultiplicative {α : Type u} [inst : Finite α] : Finite (Multiplicative α)

Equations

• @instFiniteMultiplicative = @instFiniteMultiplicative.proof_1

ink

instance instInfiniteAdditive {α : Type u} [h : Infinite α] : Infinite (Additive α)

Equations

• @instInfiniteAdditive = @instInfiniteAdditive.proof_1

ink

instance instInfiniteMultiplicative {α : Type u} [h : Infinite α] : Infinite (Multiplicative α)

Equations

• @instInfiniteMultiplicative = @instInfiniteMultiplicative.proof_1

ink

instance instNontrivialAdditive {α : Type u} [inst : Nontrivial α] : Nontrivial (Additive α)

Equations

• @instNontrivialAdditive = @instNontrivialAdditive.proof_1

ink

instance instNontrivialMultiplicative {α : Type u} [inst : Nontrivial α] : Nontrivial (Multiplicative α)

Equations

• @instNontrivialMultiplicative = @instNontrivialMultiplicative.proof_1

ink

instance Additive.add {α : Type u} [inst : Mul α] : Add (Additive α)

Equations

• Additive.add = { add := fun x y => ↑Additive.ofMul (↑Additive.toMul x * ↑Additive.toMul y) }

ink

instance Multiplicative.mul {α : Type u} [inst : Add α] : Mul (Multiplicative α)

Equations

• Multiplicative.mul = { mul := fun x y => ↑Multiplicative.ofAdd (↑Multiplicative.toAdd x + ↑Multiplicative.toAdd y) }

ink

@[simp]

theorem ofAdd_add {α : Type u} [inst : Add α] (x : α) (y : α) : ↑Multiplicative.ofAdd (x + y) = ↑Multiplicative.ofAdd x * ↑Multiplicative.ofAdd y

ink

@[simp]

theorem toAdd_mul {α : Type u} [inst : Add α] (x : Multiplicative α) (y : Multiplicative α) : ↑Multiplicative.toAdd (x * y) = ↑Multiplicative.toAdd x + ↑Multiplicative.toAdd y

ink

@[simp]

theorem ofMul_mul {α : Type u} [inst : Mul α] (x : α) (y : α) : ↑Additive.ofMul (x * y) = ↑Additive.ofMul x + ↑Additive.ofMul y

ink

@[simp]

theorem toMul_add {α : Type u} [inst : Mul α] (x : Additive α) (y : Additive α) : ↑Additive.toMul (x + y) = ↑Additive.toMul x * ↑Additive.toMul y

ink

instance Additive.addSemigroup {α : Type u} [inst : Semigroup α] : AddSemigroup (Additive α)

Equations

• Additive.addSemigroup = let src := Additive.add; AddSemigroup.mk (_ : ∀ (a b c : α), a * b * c = a * (b * c))

ink

instance Multiplicative.semigroup {α : Type u} [inst : AddSemigroup α] : Semigroup (Multiplicative α)

Equations

• Multiplicative.semigroup = let src := Multiplicative.mul; Semigroup.mk (_ : ∀ (a b c : α), a + b + c = a + (b + c))

ink

instance Additive.addCommSemigroup {α : Type u} [inst : CommSemigroup α] : AddCommSemigroup (Additive α)

Equations

• Additive.addCommSemigroup = let src := Additive.addSemigroup; AddCommSemigroup.mk (_ : ∀ (a b : α), a * b = b * a)

ink

instance Multiplicative.commSemigroup {α : Type u} [inst : AddCommSemigroup α] : CommSemigroup (Multiplicative α)

Equations

• Multiplicative.commSemigroup = let src := Multiplicative.semigroup; CommSemigroup.mk (_ : ∀ (a b : α), a + b = b + a)

ink

instance Additive.isLeftCancelAdd {α : Type u} [inst : Mul α] [inst : IsLeftCancelMul α] : IsLeftCancelAdd (Additive α)

Equations

• @Additive.isLeftCancelAdd = @Additive.isLeftCancelAdd.proof_1

ink

instance Multiplicative.isLeftCancelMul {α : Type u} [inst : Add α] [inst : IsLeftCancelAdd α] : IsLeftCancelMul (Multiplicative α)

Equations

• @Multiplicative.isLeftCancelMul = @Multiplicative.isLeftCancelMul.proof_1

ink

instance Additive.isRightCancelAdd {α : Type u} [inst : Mul α] [inst : IsRightCancelMul α] : IsRightCancelAdd (Additive α)

Equations

• @Additive.isRightCancelAdd = @Additive.isRightCancelAdd.proof_1

ink

instance Multiplicative.isRightCancelMul {α : Type u} [inst : Add α] [inst : IsRightCancelAdd α] : IsRightCancelMul (Multiplicative α)

Equations

• @Multiplicative.isRightCancelMul = @Multiplicative.isRightCancelMul.proof_1

ink

instance Additive.isCancelAdd {α : Type u} [inst : Mul α] [inst : IsCancelMul α] : IsCancelAdd (Additive α)

Equations

• @Additive.isCancelAdd = @Additive.isCancelAdd.proof_1

ink

instance Multiplicative.isCancelMul {α : Type u} [inst : Add α] [inst : IsCancelAdd α] : IsCancelMul (Multiplicative α)

Equations

• @Multiplicative.isCancelMul = @Multiplicative.isCancelMul.proof_1

ink

instance Additive.addLeftCancelSemigroup {α : Type u} [inst : LeftCancelSemigroup α] : AddLeftCancelSemigroup (Additive α)

Equations

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

ink

instance Multiplicative.leftCancelSemigroup {α : Type u} [inst : AddLeftCancelSemigroup α] : LeftCancelSemigroup (Multiplicative α)

Equations

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

ink

instance Additive.addRightCancelSemigroup {α : Type u} [inst : RightCancelSemigroup α] : AddRightCancelSemigroup (Additive α)

Equations

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

ink

instance Multiplicative.rightCancelSemigroup {α : Type u} [inst : AddRightCancelSemigroup α] : RightCancelSemigroup (Multiplicative α)

Equations

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

ink

instance instZeroAdditive {α : Type u} [inst : One α] : Zero (Additive α)

Equations

• instZeroAdditive = { zero := ↑Additive.ofMul 1 }

ink

@[simp]

theorem ofMul_one {α : Type u} [inst : One α] : ↑Additive.ofMul 1 = 0

ink

@[simp]

theorem ofMul_eq_zero {A : Type u_1} [inst : One A] {x : A} : ↑Additive.ofMul x = 0 ↔ x = 1

ink

@[simp]

theorem toMul_zero {α : Type u} [inst : One α] : ↑Additive.toMul 0 = 1

ink

instance instOneMultiplicative {α : Type u} [inst : Zero α] : One (Multiplicative α)

Equations

• instOneMultiplicative = { one := ↑Multiplicative.ofAdd 0 }

ink

@[simp]

theorem ofAdd_zero {α : Type u} [inst : Zero α] : ↑Multiplicative.ofAdd 0 = 1

ink

@[simp]

theorem ofAdd_eq_one {A : Type u_1} [inst : Zero A] {x : A} : ↑Multiplicative.ofAdd x = 1 ↔ x = 0

ink

@[simp]

theorem toAdd_one {α : Type u} [inst : Zero α] : ↑Multiplicative.toAdd 1 = 0

ink

instance Additive.addZeroClass {α : Type u} [inst : MulOneClass α] : AddZeroClass (Additive α)

Equations

• Additive.addZeroClass = AddZeroClass.mk (_ : ∀ (a : α), 1 * a = a) (_ : ∀ (a : α), a * 1 = a)

ink

instance Multiplicative.mulOneClass {α : Type u} [inst : AddZeroClass α] : MulOneClass (Multiplicative α)

Equations

• Multiplicative.mulOneClass = MulOneClass.mk (_ : ∀ (a : α), 0 + a = a) (_ : ∀ (a : α), a + 0 = a)

ink

instance Additive.addMonoid {α : Type u} [h : Monoid α] : AddMonoid (Additive α)

Equations

• Additive.addMonoid = let src := Additive.addZeroClass; let src := Additive.addSemigroup; AddMonoid.mk (_ : ∀ (a : Additive α), 0 + a = a) (_ : ∀ (a : Additive α), a + 0 = a) Monoid.npow

ink

instance Multiplicative.monoid {α : Type u} [h : AddMonoid α] : Monoid (Multiplicative α)

Equations

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

ink

instance Additive.addLeftCancelMonoid {α : Type u} [inst : LeftCancelMonoid α] : AddLeftCancelMonoid (Additive α)

Equations

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

ink

instance Multiplicative.leftCancelMonoid {α : Type u} [inst : AddLeftCancelMonoid α] : LeftCancelMonoid (Multiplicative α)

Equations

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

ink

instance Additive.addRightCancelMonoid {α : Type u} [inst : RightCancelMonoid α] : AddRightCancelMonoid (Additive α)

Equations

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

ink

instance Multiplicative.rightCancelMonoid {α : Type u} [inst : AddRightCancelMonoid α] : RightCancelMonoid (Multiplicative α)

Equations

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

ink

instance Additive.addCommMonoid {α : Type u} [inst : CommMonoid α] : AddCommMonoid (Additive α)

Equations

• Additive.addCommMonoid = let src := Additive.addMonoid; let src_1 := Additive.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : Additive α), a + b = b + a)

ink

instance Multiplicative.commMonoid {α : Type u} [inst : AddCommMonoid α] : CommMonoid (Multiplicative α)

Equations

• Multiplicative.commMonoid = let src := Multiplicative.monoid; let src_1 := Multiplicative.commSemigroup; CommMonoid.mk (_ : ∀ (a b : Multiplicative α), a * b = b * a)

ink

instance Additive.neg {α : Type u} [inst : Inv α] : Neg (Additive α)

Equations

• Additive.neg = { neg := fun x => ↑Multiplicative.ofAdd (↑Additive.toMul x)⁻¹ }

ink

@[simp]

theorem ofMul_inv {α : Type u} [inst : Inv α] (x : α) : ↑Additive.ofMul x⁻¹ = -↑Additive.ofMul x

ink

@[simp]

theorem toMul_neg {α : Type u} [inst : Inv α] (x : Additive α) : ↑Additive.toMul (-x) = (↑Additive.toMul x)⁻¹

ink

instance Multiplicative.inv {α : Type u} [inst : Neg α] : Inv (Multiplicative α)

Equations

• Multiplicative.inv = { inv := fun x => ↑Additive.ofMul (-↑Multiplicative.toAdd x) }

ink

@[simp]

theorem ofAdd_neg {α : Type u} [inst : Neg α] (x : α) : ↑Multiplicative.ofAdd (-x) = (↑Multiplicative.ofAdd x)⁻¹

ink

@[simp]

theorem toAdd_inv {α : Type u} [inst : Neg α] (x : Multiplicative α) : ↑Multiplicative.toAdd x⁻¹ = -↑Multiplicative.toAdd x

ink

instance Additive.sub {α : Type u} [inst : Div α] : Sub (Additive α)

Equations

• Additive.sub = { sub := fun x y => ↑Additive.ofMul (↑Additive.toMul x / ↑Additive.toMul y) }

ink

instance Multiplicative.div {α : Type u} [inst : Sub α] : Div (Multiplicative α)

Equations

• Multiplicative.div = { div := fun x y => ↑Multiplicative.ofAdd (↑Multiplicative.toAdd x - ↑Multiplicative.toAdd y) }

ink

@[simp]

theorem ofAdd_sub {α : Type u} [inst : Sub α] (x : α) (y : α) : ↑Multiplicative.ofAdd (x - y) = ↑Multiplicative.ofAdd x / ↑Multiplicative.ofAdd y

ink

@[simp]

theorem toAdd_div {α : Type u} [inst : Sub α] (x : Multiplicative α) (y : Multiplicative α) : ↑Multiplicative.toAdd (x / y) = ↑Multiplicative.toAdd x - ↑Multiplicative.toAdd y

ink

@[simp]

theorem ofMul_div {α : Type u} [inst : Div α] (x : α) (y : α) : ↑Additive.ofMul (x / y) = ↑Additive.ofMul x - ↑Additive.ofMul y

ink

@[simp]

theorem toMul_sub {α : Type u} [inst : Div α] (x : Additive α) (y : Additive α) : ↑Additive.toMul (x - y) = ↑Additive.toMul x / ↑Additive.toMul y

ink

instance Additive.involutiveNeg {α : Type u} [inst : InvolutiveInv α] : InvolutiveNeg (Additive α)

Equations

• Additive.involutiveNeg = let src := Additive.neg; InvolutiveNeg.mk (_ : ∀ (a : α), a⁻¹⁻¹ = a)

ink

instance Multiplicative.involutiveInv {α : Type u} [inst : InvolutiveNeg α] : InvolutiveInv (Multiplicative α)

Equations

• Multiplicative.involutiveInv = let src := Multiplicative.inv; InvolutiveInv.mk (_ : ∀ (a : α), - -a = a)

ink

instance Additive.subNegMonoid {α : Type u} [inst : DivInvMonoid α] : SubNegMonoid (Additive α)

Equations

• Additive.subNegMonoid = let src := Additive.neg; let src_1 := Additive.sub; let src_2 := Additive.addMonoid; SubNegMonoid.mk DivInvMonoid.zpow

ink

instance Multiplicative.divInvMonoid {α : Type u} [inst : SubNegMonoid α] : DivInvMonoid (Multiplicative α)

Equations

• Multiplicative.divInvMonoid = let src := Multiplicative.inv; let src_1 := Multiplicative.div; let src_2 := Multiplicative.monoid; DivInvMonoid.mk SubNegMonoid.zsmul

ink

instance Additive.subtractionMonoid {α : Type u} [inst : DivisionMonoid α] : SubtractionMonoid (Additive α)

Equations

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

ink

instance Multiplicative.divisionMonoid {α : Type u} [inst : SubtractionMonoid α] : DivisionMonoid (Multiplicative α)

Equations

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

ink

instance Additive.subtractionCommMonoid {α : Type u} [inst : DivisionCommMonoid α] : SubtractionCommMonoid (Additive α)

Equations

• Additive.subtractionCommMonoid = let src := Additive.subtractionMonoid; let src_1 := Additive.addCommSemigroup; SubtractionCommMonoid.mk (_ : ∀ (a b : Additive α), a + b = b + a)

ink

instance Multiplicative.divisionCommMonoid {α : Type u} [inst : SubtractionCommMonoid α] : DivisionCommMonoid (Multiplicative α)

Equations

• Multiplicative.divisionCommMonoid = let src := Multiplicative.divisionMonoid; let src_1 := Multiplicative.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : Multiplicative α), a * b = b * a)

ink

instance Additive.addGroup {α : Type u} [inst : Group α] : AddGroup (Additive α)

Equations

• Additive.addGroup = let src := Additive.subNegMonoid; AddGroup.mk (_ : ∀ (a : α), a⁻¹ * a = 1)

ink

instance Multiplicative.group {α : Type u} [inst : AddGroup α] : Group (Multiplicative α)

Equations

• Multiplicative.group = let src := Multiplicative.divInvMonoid; Group.mk (_ : ∀ (a : α), -a + a = 0)

ink

instance Additive.addCommGroup {α : Type u} [inst : CommGroup α] : AddCommGroup (Additive α)

Equations

• Additive.addCommGroup = let src := Additive.addGroup; let src_1 := Additive.addCommMonoid; AddCommGroup.mk (_ : ∀ (a b : Additive α), a + b = b + a)

ink

instance Multiplicative.commGroup {α : Type u} [inst : AddCommGroup α] : CommGroup (Multiplicative α)

Equations

• Multiplicative.commGroup = let src := Multiplicative.group; let src_1 := Multiplicative.commMonoid; CommGroup.mk (_ : ∀ (a b : Multiplicative α), a * b = b * a)

ink

@[simp]

theorem AddMonoidHom.toMultiplicative_symm_apply_apply {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : AddZeroClass β] (f : Multiplicative α →* Multiplicative β) (a : α) : ↑(↑(Equiv.symm AddMonoidHom.toMultiplicative) f) a = ↑Multiplicative.toAdd (↑f (↑Multiplicative.ofAdd a))

ink

@[simp]

theorem AddMonoidHom.toMultiplicative_apply_apply {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : AddZeroClass β] (f : α →+ β) (a : Multiplicative α) : ↑(↑AddMonoidHom.toMultiplicative f) a = ↑Multiplicative.ofAdd (↑f (↑Multiplicative.toAdd a))

ink

def AddMonoidHom.toMultiplicative {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : AddZeroClass β] : (α →+ β) ≃ (Multiplicative α →* Multiplicative β)

Reinterpret α →+ β→+ β as Multiplicative α →* Multiplicative β→* Multiplicative β.

Equations

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

ink

@[simp]

theorem MonoidHom.toAdditive_apply_apply {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : MulOneClass β] (f : α →* β) (a : Additive α) : ↑(↑MonoidHom.toAdditive f) a = ↑Additive.ofMul (↑f (↑Additive.toMul a))

ink

@[simp]

theorem MonoidHom.toAdditive_symm_apply_apply {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : MulOneClass β] (f : Additive α →+ Additive β) (a : α) : ↑(↑(Equiv.symm MonoidHom.toAdditive) f) a = ↑Additive.toMul (↑f (↑Additive.ofMul a))

ink

def MonoidHom.toAdditive {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : MulOneClass β] : (α →* β) ≃ (Additive α →+ Additive β)

Reinterpret α →* β→* β as Additive α →+ Additive β→+ Additive β.

Equations

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

ink

@[simp]

theorem AddMonoidHom.toMultiplicative'_apply_apply {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : AddZeroClass β] (f : Additive α →+ β) (a : α) : ↑(↑AddMonoidHom.toMultiplicative' f) a = ↑Multiplicative.ofAdd (↑f (↑Additive.ofMul a))

ink

@[simp]

theorem AddMonoidHom.toMultiplicative'_symm_apply_apply {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : AddZeroClass β] (f : α →* Multiplicative β) (a : Additive α) : ↑(↑(Equiv.symm AddMonoidHom.toMultiplicative') f) a = ↑Multiplicative.toAdd (↑f (↑Additive.toMul a))

ink

def AddMonoidHom.toMultiplicative' {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : AddZeroClass β] : (Additive α →+ β) ≃ (α →* Multiplicative β)

Reinterpret Additive α →+ β→+ β as α →* Multiplicative β→* Multiplicative β.

Equations

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

ink

@[simp]

theorem MonoidHom.toAdditive'_symm_apply_apply {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : AddZeroClass β] : ∀ (a : Additive α →+ β) (a_1 : α), ↑(↑(Equiv.symm MonoidHom.toAdditive') a) a_1 = ↑Multiplicative.ofAdd (↑a (↑Additive.ofMul a_1))

ink

@[simp]

theorem MonoidHom.toAdditive'_apply_apply {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : AddZeroClass β] : ∀ (a : α →* Multiplicative β) (a_1 : Additive α), ↑(↑MonoidHom.toAdditive' a) a_1 = ↑Multiplicative.toAdd (↑a (↑Additive.toMul a_1))

ink

def MonoidHom.toAdditive' {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : AddZeroClass β] : (α →* Multiplicative β) ≃ (Additive α →+ β)

Reinterpret α →* Multiplicative β→* Multiplicative β as Additive α →+ β→+ β.

Equations

• MonoidHom.toAdditive' = Equiv.symm AddMonoidHom.toMultiplicative'

ink

@[simp]

theorem AddMonoidHom.toMultiplicative''_apply_apply {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : MulOneClass β] (f : α →+ Additive β) (a : Multiplicative α) : ↑(↑AddMonoidHom.toMultiplicative'' f) a = ↑Additive.toMul (↑f (↑Multiplicative.toAdd a))

ink

@[simp]

theorem AddMonoidHom.toMultiplicative''_symm_apply_apply {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : MulOneClass β] (f : Multiplicative α →* β) (a : α) : ↑(↑(Equiv.symm AddMonoidHom.toMultiplicative'') f) a = ↑Additive.ofMul (↑f (↑Multiplicative.ofAdd a))

ink

def AddMonoidHom.toMultiplicative'' {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : MulOneClass β] : (α →+ Additive β) ≃ (Multiplicative α →* β)

Reinterpret α →+ Additive β→+ Additive β as Multiplicative α →* β→* β.

Equations

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

ink

@[simp]

theorem MonoidHom.toAdditive''_apply_apply {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : MulOneClass β] : ∀ (a : Multiplicative α →* β) (a_1 : α), ↑(↑MonoidHom.toAdditive'' a) a_1 = ↑Additive.ofMul (↑a (↑Multiplicative.ofAdd a_1))

ink

@[simp]

theorem MonoidHom.toAdditive''_symm_apply_apply {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : MulOneClass β] : ∀ (a : α →+ Additive β) (a_1 : Multiplicative α), ↑(↑(Equiv.symm MonoidHom.toAdditive'') a) a_1 = ↑Additive.toMul (↑a (↑Multiplicative.toAdd a_1))

ink

def MonoidHom.toAdditive'' {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : MulOneClass β] : (Multiplicative α →* β) ≃ (α →+ Additive β)

Reinterpret Multiplicative α →* β→* β as α →+ Additive β→+ Additive β.

Equations

• MonoidHom.toAdditive'' = Equiv.symm AddMonoidHom.toMultiplicative''

ink

instance Additive.coeToFun {α : Type u_1} {β : α → Sort u_2} [inst : CoeFun α β] : CoeFun (Additive α) fun a => β (↑Additive.toMul a)

If α has some multiplicative structure and coerces to a function, then Additive α should also coerce to the same function.

This allows Additive to be used on bundled function types with a multiplicative structure, which is often used for composition, without affecting the behavior of the function itself.

Equations

• Additive.coeToFun = { coe := fun a => CoeFun.coe (↑Additive.toMul a) }

ink

instance Multiplicative.coeToFun {α : Type u_1} {β : α → Sort u_2} [inst : CoeFun α β] : CoeFun (Multiplicative α) fun a => β (↑Multiplicative.toAdd a)

If α has some additive structure and coerces to a function, then Multiplicative α should also coerce to the same function.

This allows Multiplicative to be used on bundled function types with an additive structure, which is often used for composition, without affecting the behavior of the function itself.

Equations

• Multiplicative.coeToFun = { coe := fun a => CoeFun.coe (↑Multiplicative.toAdd a) }