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.

def Additive (α : Type u_1) : Type u_1

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

Equations

• Additive α = α

def Multiplicative (α : Type u_1) : Type u_1

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

Equations

• Multiplicative α = α

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

Reinterpret x : α as an element of Additive α.

Equations

• Additive.ofMul = { toFun := fun (x : α) => x, invFun := fun (x : Additive α) => x, left_inv := ⋯, right_inv := ⋯ }

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

Reinterpret x : Additive α as an element of α.

Equations

• Additive.toMul = Additive.ofMul.symm

@[simp]

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

@[simp]

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

@[simp]

theorem Additive.forall {α : Type u} {p : Additive α → Prop} : (∀ (a : Additive α), p a) ↔ ∀ (a : α), p (Additive.ofMul a)

@[simp]

theorem Additive.exists {α : Type u} {p : Additive α → Prop} : (∃ (a : Additive α), p a) ↔ ∃ (a : α), p (Additive.ofMul a)

def Additive.rec {α : Type u} {motive : Additive α → Sort u_1} (ofMul : (a : α) → motive (Additive.ofMul a)) (a : Additive α) : motive a

Recursion principle for Additive, supported by cases and induction.

Equations

• Additive.rec ofMul a = ofMul (Additive.toMul a)

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

Reinterpret x : α as an element of Multiplicative α.

Equations

• Multiplicative.ofAdd = { toFun := fun (x : α) => x, invFun := fun (x : Multiplicative α) => x, left_inv := ⋯, right_inv := ⋯ }

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

Reinterpret x : Multiplicative α as an element of α.

Equations

• Multiplicative.toAdd = Multiplicative.ofAdd.symm

@[simp]

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

@[simp]

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

@[simp]

theorem Multiplicative.forall {α : Type u} {p : Multiplicative α → Prop} : (∀ (a : Multiplicative α), p a) ↔ ∀ (a : α), p (Multiplicative.ofAdd a)

@[simp]

theorem Multiplicative.exists {α : Type u} {p : Multiplicative α → Prop} : (∃ (a : Multiplicative α), p a) ↔ ∃ (a : α), p (Multiplicative.ofAdd a)

def Multiplicative.rec {α : Type u} {motive : Multiplicative α → Sort u_1} (ofAdd : (a : α) → motive (Multiplicative.ofAdd a)) (a : Multiplicative α) : motive a

Recursion principle for Multiplicative, supported by cases and induction.

Equations

• Multiplicative.rec ofAdd a = ofAdd (Multiplicative.toAdd a)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance instSubsingletonAdditive {α : Type u} [Subsingleton α] : Subsingleton (Additive α)

instance instSubsingletonMultiplicative {α : Type u} [Subsingleton α] : Subsingleton (Multiplicative α)

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

Equations

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

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

Equations

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

instance instUniqueAdditive {α : Type u} [Unique α] : Unique (Additive α)

Equations

• instUniqueAdditive = Additive.toMul.unique

instance instUniqueMultiplicative {α : Type u} [Unique α] : Unique (Multiplicative α)

Equations

• instUniqueMultiplicative = Multiplicative.toAdd.unique

instance instDecidableEqMultiplicative {α : Type u} [h : DecidableEq α] : DecidableEq (Multiplicative α)

Equations

• instDecidableEqMultiplicative = h

instance instDecidableEqAdditive {α : Type u} [h : DecidableEq α] : DecidableEq (Additive α)

Equations

• instDecidableEqAdditive = h

instance Additive.instNontrivial {α : Type u} [Nontrivial α] : Nontrivial (Additive α)

instance Multiplicative.instNontrivial {α : Type u} [Nontrivial α] : Nontrivial (Multiplicative α)

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• Additive.addSemigroup = AddSemigroup.mk ⋯

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

Equations

• Multiplicative.semigroup = Semigroup.mk ⋯

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

Equations

• Additive.addCommSemigroup = AddCommSemigroup.mk ⋯

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

Equations

• Multiplicative.commSemigroup = CommSemigroup.mk ⋯

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

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

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

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

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

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

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

Equations

• Additive.addLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯

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

Equations

• Multiplicative.leftCancelSemigroup = LeftCancelSemigroup.mk ⋯

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

Equations

• Additive.addRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯

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

Equations

• Multiplicative.rightCancelSemigroup = RightCancelSemigroup.mk ⋯

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

Equations

• instZeroAdditiveOfOne = { zero := Additive.ofMul 1 }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem toMul_eq_one {α : Type u_1} [One α] {x : Additive α} : Additive.toMul x = 1 ↔ x = 0

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

Equations

• instOneMultiplicativeOfZero = { one := Multiplicative.ofAdd 0 }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem toAdd_eq_zero {α : Type u_1} [Zero α] {x : Multiplicative α} : Multiplicative.toAdd x = 0 ↔ x = 1

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

Equations

• Additive.addZeroClass = AddZeroClass.mk ⋯ ⋯

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

Equations

• Multiplicative.mulOneClass = MulOneClass.mk ⋯ ⋯

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

Equations

• Additive.addMonoid = AddMonoid.mk ⋯ ⋯ Monoid.npow ⋯ ⋯

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

Equations

• Multiplicative.monoid = Monoid.mk ⋯ ⋯ AddMonoid.nsmul ⋯ ⋯

@[simp]

theorem ofMul_pow {α : Type u} [Monoid α] (n : ℕ) (a : α) : Additive.ofMul (a ^ n) = n • Additive.ofMul a

@[simp]

theorem toMul_nsmul {α : Type u} [Monoid α] (n : ℕ) (a : Additive α) : Additive.toMul (n • a) = Additive.toMul a ^ n

@[simp]

theorem ofAdd_nsmul {α : Type u} [AddMonoid α] (n : ℕ) (a : α) : Multiplicative.ofAdd (n • a) = Multiplicative.ofAdd a ^ n

@[simp]

theorem toAdd_pow {α : Type u} [AddMonoid α] (a : Multiplicative α) (n : ℕ) : Multiplicative.toAdd (a ^ n) = n • Multiplicative.toAdd a

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

Equations

• Additive.addLeftCancelMonoid = AddLeftCancelMonoid.mk ⋯

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

Equations

• Multiplicative.leftCancelMonoid = LeftCancelMonoid.mk ⋯

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

Equations

• Additive.addRightCancelMonoid = AddRightCancelMonoid.mk ⋯

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

Equations

• Multiplicative.rightCancelMonoid = RightCancelMonoid.mk ⋯

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

Equations

• Additive.addCommMonoid = AddCommMonoid.mk ⋯

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

Equations

• Multiplicative.commMonoid = CommMonoid.mk ⋯

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• Additive.involutiveNeg = InvolutiveNeg.mk ⋯

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

Equations

• Multiplicative.involutiveInv = InvolutiveInv.mk ⋯

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

Equations

• Additive.subNegMonoid = SubNegMonoid.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯

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

Equations

• Multiplicative.divInvMonoid = DivInvMonoid.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯

@[simp]

theorem ofMul_zpow {α : Type u} [DivInvMonoid α] (z : ℤ) (a : α) : Additive.ofMul (a ^ z) = z • Additive.ofMul a

@[simp]

theorem toMul_zsmul {α : Type u} [DivInvMonoid α] (z : ℤ) (a : Additive α) : Additive.toMul (z • a) = Additive.toMul a ^ z

@[simp]

theorem ofAdd_zsmul {α : Type u} [SubNegMonoid α] (z : ℤ) (a : α) : Multiplicative.ofAdd (z • a) = Multiplicative.ofAdd a ^ z

@[simp]

theorem toAdd_zpow {α : Type u} [SubNegMonoid α] (a : Multiplicative α) (z : ℤ) : Multiplicative.toAdd (a ^ z) = z • Multiplicative.toAdd a

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

Equations

• Additive.subtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯

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

Equations

• Multiplicative.divisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯

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

Equations

• Additive.subtractionCommMonoid = SubtractionCommMonoid.mk ⋯

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

Equations

• Multiplicative.divisionCommMonoid = DivisionCommMonoid.mk ⋯

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

Equations

• Additive.addGroup = AddGroup.mk ⋯

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

Equations

• Multiplicative.group = Group.mk ⋯

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

Equations

• Additive.addCommGroup = AddCommGroup.mk ⋯

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

Equations

• Multiplicative.commGroup = CommGroup.mk ⋯

instance Additive.coeToFun {α : Type u_1} {β : α → Sort u_2} [CoeFun α β] : CoeFun (Additive α) fun (a : Additive α) => β (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 : Additive α) => CoeFun.coe (Additive.toMul a) }

instance Multiplicative.coeToFun {α : Type u_1} {β : α → Sort u_2} [CoeFun α β] : CoeFun (Multiplicative α) fun (a : Multiplicative α) => β (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 : Multiplicative α) => CoeFun.coe (Multiplicative.toAdd a) }

theorem Pi.mulSingle_multiplicativeOfAdd_eq {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] (i : ι) (a : M i) (j : ι) : Pi.mulSingle i (Multiplicative.ofAdd a) j = Multiplicative.ofAdd (Pi.single i a j)

theorem Pi.single_additiveOfMul_eq {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} [(i : ι) → Monoid (M i)] (i : ι) (a : M i) (j : ι) : Pi.single i (Additive.ofMul a) j = Additive.ofMul (Pi.mulSingle i a j)