Documentation

Mathlib.Algebra.Group.TypeTags

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

We define two type tags:

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

See also #

This file is similar to Order.Synonym.

Porting notes #

def Additive (α : Type u_1) :
Type u_1

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

Equations
def Multiplicative (α : Type u_1) :
Type u_1

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

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

Reinterpret x : α as an element of Additive α.

Equations
  • One or more equations did not get rendered due to their size.
def Additive.toMul {α : Type u} :

Reinterpret x : Additive α as an element of α.

Equations
@[simp]
theorem Additive.ofMul_symm_eq {α : Type u} :
Equiv.symm Additive.ofMul = Additive.toMul
@[simp]
theorem Additive.toMul_symm_eq {α : Type u} :
Equiv.symm Additive.toMul = Additive.ofMul

Reinterpret x : α as an element of Multiplicative α.

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

Reinterpret x : Multiplicative α as an element of α.

Equations
@[simp]
theorem Multiplicative.ofAdd_symm_eq {α : Type u} :
Equiv.symm Multiplicative.ofAdd = Multiplicative.toAdd
@[simp]
theorem Multiplicative.toAdd_symm_eq {α : Type u} :
Equiv.symm Multiplicative.toAdd = Multiplicative.ofAdd
@[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 instInhabitedAdditive {α : Type u} [inst : Inhabited α] :
Equations
  • instInhabitedAdditive = { default := Additive.ofMul default }
Equations
  • instInhabitedMultiplicative = { default := Multiplicative.ofAdd default }
instance Additive.add {α : Type u} [inst : Mul α] :
Equations
  • Additive.add = { add := fun x y => Additive.ofMul (Additive.toMul x * Additive.toMul y) }
instance Multiplicative.mul {α : Type u} [inst : Add α] :
Equations
  • Multiplicative.mul = { mul := fun x y => Multiplicative.ofAdd (Multiplicative.toAdd x + Multiplicative.toAdd y) }
@[simp]
theorem ofAdd_add {α : Type u} [inst : Add α] (x : α) (y : α) :
Multiplicative.ofAdd (x + y) = Multiplicative.ofAdd x * Multiplicative.ofAdd y
@[simp]
theorem toAdd_mul {α : Type u} [inst : Add α] (x : Multiplicative α) (y : Multiplicative α) :
Multiplicative.toAdd (x * y) = Multiplicative.toAdd x + Multiplicative.toAdd y
@[simp]
theorem ofMul_mul {α : Type u} [inst : Mul α] (x : α) (y : α) :
Additive.ofMul (x * y) = Additive.ofMul x + Additive.ofMul y
@[simp]
theorem toMul_add {α : Type u} [inst : Mul α] (x : Additive α) (y : Additive α) :
Additive.toMul (x + y) = Additive.toMul x * Additive.toMul y
instance Additive.addSemigroup {α : Type u} [inst : Semigroup α] :
Equations
  • Additive.addSemigroup = let src := Additive.add; AddSemigroup.mk (_ : ∀ (a b c : α), a * b * c = a * (b * c))
Equations
  • Multiplicative.semigroup = let src := Multiplicative.mul; Semigroup.mk (_ : ∀ (a b c : α), a + b + c = a + (b + c))
Equations
  • Additive.addCommSemigroup = let src := Additive.addSemigroup; AddCommSemigroup.mk (_ : ∀ (a b : α), a * b = b * a)
Equations
  • Multiplicative.commSemigroup = let src := Multiplicative.semigroup; CommSemigroup.mk (_ : ∀ (a b : α), a + b = b + a)
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
instance instZeroAdditive {α : Type u} [inst : One α] :
Equations
  • instZeroAdditive = { zero := Additive.ofMul 1 }
@[simp]
theorem ofMul_one {α : Type u} [inst : One α] :
Additive.ofMul 1 = 0
@[simp]
theorem ofMul_eq_zero {A : Type u_1} [inst : One A] {x : A} :
Additive.ofMul x = 0 x = 1
@[simp]
theorem toMul_zero {α : Type u} [inst : One α] :
Additive.toMul 0 = 1
instance instOneMultiplicative {α : Type u} [inst : Zero α] :
Equations
  • instOneMultiplicative = { one := Multiplicative.ofAdd 0 }
@[simp]
theorem ofAdd_zero {α : Type u} [inst : Zero α] :
Multiplicative.ofAdd 0 = 1
@[simp]
theorem ofAdd_eq_one {A : Type u_1} [inst : Zero A] {x : A} :
Multiplicative.ofAdd x = 1 x = 0
@[simp]
theorem toAdd_one {α : Type u} [inst : Zero α] :
Multiplicative.toAdd 1 = 0
instance Additive.addZeroClass {α : Type u} [inst : MulOneClass α] :
Equations
Equations
  • Multiplicative.mulOneClass = MulOneClass.mk (_ : ∀ (a : α), 0 + a = a) (_ : ∀ (a : α), a + 0 = a)
instance Additive.addMonoid {α : Type u} [h : Monoid α] :
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
instance Multiplicative.monoid {α : Type u} [h : AddMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
instance Additive.addCommMonoid {α : Type u} [inst : CommMonoid α] :
Equations
  • Additive.addCommMonoid = let src := Additive.addMonoid; let src_1 := Additive.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : Additive α), a + b = b + a)
Equations
  • Multiplicative.commMonoid = let src := Multiplicative.monoid; let src_1 := Multiplicative.commSemigroup; CommMonoid.mk (_ : ∀ (a b : Multiplicative α), a * b = b * a)
instance Additive.neg {α : Type u} [inst : Inv α] :
Equations
  • Additive.neg = { neg := fun x => Multiplicative.ofAdd (Additive.toMul x)⁻¹ }
@[simp]
theorem ofMul_inv {α : Type u} [inst : Inv α] (x : α) :
Additive.ofMul x⁻¹ = -Additive.ofMul x
@[simp]
theorem toMul_neg {α : Type u} [inst : Inv α] (x : Additive α) :
Additive.toMul (-x) = (Additive.toMul x)⁻¹
instance Multiplicative.inv {α : Type u} [inst : Neg α] :
Equations
  • Multiplicative.inv = { inv := fun x => Additive.ofMul (-Multiplicative.toAdd x) }
@[simp]
theorem ofAdd_neg {α : Type u} [inst : Neg α] (x : α) :
Multiplicative.ofAdd (-x) = (Multiplicative.ofAdd x)⁻¹
@[simp]
theorem toAdd_inv {α : Type u} [inst : Neg α] (x : Multiplicative α) :
Multiplicative.toAdd x⁻¹ = -Multiplicative.toAdd x
instance Additive.sub {α : Type u} [inst : Div α] :
Equations
  • Additive.sub = { sub := fun x y => Additive.ofMul (Additive.toMul x / Additive.toMul y) }
instance Multiplicative.div {α : Type u} [inst : Sub α] :
Equations
  • Multiplicative.div = { div := fun x y => Multiplicative.ofAdd (Multiplicative.toAdd x - Multiplicative.toAdd y) }
@[simp]
theorem ofAdd_sub {α : Type u} [inst : Sub α] (x : α) (y : α) :
Multiplicative.ofAdd (x - y) = Multiplicative.ofAdd x / Multiplicative.ofAdd y
@[simp]
theorem toAdd_div {α : Type u} [inst : Sub α] (x : Multiplicative α) (y : Multiplicative α) :
Multiplicative.toAdd (x / y) = Multiplicative.toAdd x - Multiplicative.toAdd y
@[simp]
theorem ofMul_div {α : Type u} [inst : Div α] (x : α) (y : α) :
Additive.ofMul (x / y) = Additive.ofMul x - Additive.ofMul y
@[simp]
theorem toMul_sub {α : Type u} [inst : Div α] (x : Additive α) (y : Additive α) :
Additive.toMul (x - y) = Additive.toMul x / Additive.toMul y
instance Additive.involutiveNeg {α : Type u} [inst : InvolutiveInv α] :
Equations
Equations
  • Multiplicative.involutiveInv = let src := Multiplicative.inv; InvolutiveInv.mk (_ : ∀ (a : α), - -a = a)
instance Additive.subNegMonoid {α : Type u} [inst : DivInvMonoid α] :
Equations
  • Additive.subNegMonoid = let src := Additive.neg; let src_1 := Additive.sub; let src_2 := Additive.addMonoid; SubNegMonoid.mk DivInvMonoid.zpow
Equations
  • Multiplicative.divInvMonoid = let src := Multiplicative.inv; let src_1 := Multiplicative.div; let src_2 := Multiplicative.monoid; DivInvMonoid.mk SubNegMonoid.zsmul
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Additive.subtractionCommMonoid = let src := Additive.subtractionMonoid; let src_1 := Additive.addCommSemigroup; SubtractionCommMonoid.mk (_ : ∀ (a b : Additive α), a + b = b + a)
Equations
instance Additive.addGroup {α : Type u} [inst : Group α] :
Equations
  • Additive.addGroup = let src := Additive.subNegMonoid; AddGroup.mk (_ : ∀ (a : α), a⁻¹ * a = 1)
instance Multiplicative.group {α : Type u} [inst : AddGroup α] :
Equations
  • Multiplicative.group = let src := Multiplicative.divInvMonoid; Group.mk (_ : ∀ (a : α), -a + a = 0)
instance Additive.addCommGroup {α : Type u} [inst : CommGroup α] :
Equations
  • Additive.addCommGroup = let src := Additive.addGroup; let src_1 := Additive.addCommMonoid; AddCommGroup.mk (_ : ∀ (a b : Additive α), a + b = b + a)
Equations
  • Multiplicative.commGroup = let src := Multiplicative.group; let src_1 := Multiplicative.commMonoid; CommGroup.mk (_ : ∀ (a b : Multiplicative α), a * b = b * a)
@[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))
@[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))
def AddMonoidHom.toMultiplicative {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : AddZeroClass β] :

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

Equations
  • One or more equations did not get rendered due to their size.
@[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))
@[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))
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.
@[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))
@[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))
def AddMonoidHom.toMultiplicative' {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : AddZeroClass β] :

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

Equations
  • One or more equations did not get rendered due to their size.
@[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))
@[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))
def MonoidHom.toAdditive' {α : Type u} {β : Type v} [inst : MulOneClass α] [inst : AddZeroClass β] :

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

Equations
  • MonoidHom.toAdditive' = Equiv.symm AddMonoidHom.toMultiplicative'
@[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))
@[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))
def AddMonoidHom.toMultiplicative'' {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : MulOneClass β] :

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

Equations
  • One or more equations did not get rendered due to their size.
@[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))
@[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))
def MonoidHom.toAdditive'' {α : Type u} {β : Type v} [inst : AddZeroClass α] [inst : MulOneClass β] :

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

Equations
  • MonoidHom.toAdditive'' = Equiv.symm AddMonoidHom.toMultiplicative''
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) }
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) }