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
Instances For
    def Multiplicative (α : Type u_1) :
    Type u_1

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

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

      Reinterpret x : α as an element of Additive α.

      Equations
      • Additive.ofMul = { toFun := fun (x : α) => x, invFun := fun (x : Additive α) => x, left_inv := , right_inv := }
      Instances For
        def Additive.toMul {α : Type u} :

        Reinterpret x : Additive α as an element of α.

        Equations
        • Additive.toMul = Additive.ofMul.symm
        Instances For
          @[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
          Instances For

            Reinterpret x : α as an element of Multiplicative α.

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

              Reinterpret x : Multiplicative α as an element of α.

              Equations
              • Multiplicative.toAdd = Multiplicative.ofAdd.symm
              Instances For
                @[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
                Instances For
                  @[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
                  Equations
                  • =
                  Equations
                  • instInhabitedAdditive = { default := Additive.ofMul default }
                  Equations
                  • instInhabitedMultiplicative = { default := Multiplicative.ofAdd default }
                  instance instUniqueAdditive {α : Type u} [Unique α] :
                  Equations
                  • instUniqueAdditive = Additive.toMul.unique
                  Equations
                  • instUniqueMultiplicative = Multiplicative.toAdd.unique
                  instance instFiniteAdditive {α : Type u} [Finite α] :
                  Equations
                  • =
                  Equations
                  • =
                  instance instInfiniteAdditive {α : Type u} [h : Infinite α] :
                  Equations
                  • = h
                  Equations
                  • = h
                  Equations
                  • instDecidableEqMultiplicative = h
                  Equations
                  • instDecidableEqAdditive = h
                  Equations
                  • =
                  Equations
                  • =
                  instance Additive.add {α : Type u} [Mul α] :
                  Equations
                  • Additive.add = { add := fun (x y : Additive α) => Additive.ofMul (Additive.toMul x * Additive.toMul y) }
                  instance Multiplicative.mul {α : Type u} [Add α] :
                  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 : Multiplicative α) (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 : Additive α) (y : Additive α) :
                  Additive.toMul (x + y) = Additive.toMul x * Additive.toMul y
                  Equations
                  Equations
                  • Multiplicative.semigroup = let __src := Multiplicative.mul; Semigroup.mk
                  Equations
                  Equations
                  • Multiplicative.commSemigroup = let __src := Multiplicative.semigroup; CommSemigroup.mk
                  Equations
                  • =
                  Equations
                  • =
                  instance Additive.isCancelAdd {α : Type u} [Mul α] [IsCancelMul α] :
                  Equations
                  • =
                  Equations
                  • =
                  Equations
                  Equations
                  • Multiplicative.leftCancelSemigroup = let __src := Multiplicative.semigroup; let __src_1 := ; LeftCancelSemigroup.mk
                  Equations
                  Equations
                  • Multiplicative.rightCancelSemigroup = let __src := Multiplicative.semigroup; let __src_1 := ; RightCancelSemigroup.mk
                  instance instZeroAdditiveOfOne {α : Type u} [One α] :
                  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
                  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
                  Equations
                  Equations
                  instance Additive.addMonoid {α : Type u} [h : Monoid α] :
                  Equations
                  • Additive.addMonoid = let __src := Additive.addZeroClass; let __src_1 := Additive.addSemigroup; AddMonoid.mk Monoid.npow
                  instance Multiplicative.monoid {α : Type u} [h : AddMonoid α] :
                  Equations
                  • Multiplicative.monoid = let __src := Multiplicative.mulOneClass; let __src_1 := Multiplicative.semigroup; 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
                  Equations
                  • Additive.addLeftCancelMonoid = let __src := Additive.addMonoid; let __src_1 := Additive.addLeftCancelSemigroup; AddLeftCancelMonoid.mk AddMonoid.nsmul
                  Equations
                  • Multiplicative.leftCancelMonoid = let __src := Multiplicative.monoid; let __src_1 := Multiplicative.leftCancelSemigroup; LeftCancelMonoid.mk Monoid.npow
                  Equations
                  • Additive.addRightCancelMonoid = let __src := Additive.addMonoid; let __src_1 := Additive.addRightCancelSemigroup; AddRightCancelMonoid.mk AddMonoid.nsmul
                  Equations
                  • Multiplicative.rightCancelMonoid = let __src := Multiplicative.monoid; let __src_1 := Multiplicative.rightCancelSemigroup; RightCancelMonoid.mk Monoid.npow
                  Equations
                  • Additive.addCommMonoid = let __src := Additive.addMonoid; let __src_1 := Additive.addCommSemigroup; AddCommMonoid.mk
                  Equations
                  • Multiplicative.commMonoid = let __src := Multiplicative.monoid; let __src_1 := Multiplicative.commSemigroup; CommMonoid.mk
                  instance Additive.neg {α : Type u} [Inv α] :
                  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 α] :
                  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 α] :
                  Equations
                  • Additive.sub = { sub := fun (x y : Additive α) => Additive.ofMul (Additive.toMul x / Additive.toMul y) }
                  instance Multiplicative.div {α : Type u} [Sub α] :
                  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 : Multiplicative α) (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 : Additive α) (y : Additive α) :
                  Additive.toMul (x - y) = Additive.toMul x / Additive.toMul y
                  Equations
                  Equations
                  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
                  @[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
                  Equations
                  • Additive.subtractionMonoid = let __src := Additive.subNegMonoid; let __src_1 := Additive.involutiveNeg; SubtractionMonoid.mk
                  Equations
                  • Multiplicative.divisionMonoid = let __src := Multiplicative.divInvMonoid; let __src_1 := Multiplicative.involutiveInv; DivisionMonoid.mk
                  Equations
                  • Additive.subtractionCommMonoid = let __src := Additive.subtractionMonoid; let __src_1 := Additive.addCommSemigroup; SubtractionCommMonoid.mk
                  Equations
                  • Multiplicative.divisionCommMonoid = let __src := Multiplicative.divisionMonoid; let __src_1 := Multiplicative.commSemigroup; DivisionCommMonoid.mk
                  instance Additive.addGroup {α : Type u} [Group α] :
                  Equations
                  • Additive.addGroup = let __src := Additive.subNegMonoid; AddGroup.mk
                  Equations
                  • Multiplicative.group = let __src := Multiplicative.divInvMonoid; Group.mk
                  Equations
                  • Additive.addCommGroup = let __src := Additive.addGroup; let __src_1 := Additive.addCommMonoid; AddCommGroup.mk
                  Equations
                  • Multiplicative.commGroup = let __src := Multiplicative.group; let __src_1 := Multiplicative.commMonoid; CommGroup.mk
                  @[simp]
                  theorem AddMonoidHom.toMultiplicative_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (a : Multiplicative α) :
                  (AddMonoidHom.toMultiplicative f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))
                  @[simp]
                  theorem AddMonoidHom.toMultiplicative_symm_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] (f : Multiplicative α →* Multiplicative β) (a : α) :
                  (AddMonoidHom.toMultiplicative.symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem AddMonoidHom.coe_toMultiplicative {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) :
                    (AddMonoidHom.toMultiplicative f) = Multiplicative.ofAdd f Multiplicative.toAdd
                    @[simp]
                    theorem MonoidHom.toAdditive_symm_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] (f : Additive α →+ Additive β) (a : α) :
                    (MonoidHom.toAdditive.symm f) a = Additive.toMul (f (Additive.ofMul a))
                    @[simp]
                    theorem MonoidHom.toAdditive_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] (f : α →* β) (a : Additive α) :
                    (MonoidHom.toAdditive f) a = Additive.ofMul (f (Additive.toMul a))
                    def MonoidHom.toAdditive {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] :
                    (α →* β) (Additive α →+ Additive β)

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem MonoidHom.coe_toMultiplicative {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] (f : α →* β) :
                      (MonoidHom.toAdditive f) = Additive.ofMul f Additive.toMul
                      @[simp]
                      theorem AddMonoidHom.toMultiplicative'_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [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} [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) (a : Additive α) :
                      (AddMonoidHom.toMultiplicative'.symm f) a = Multiplicative.toAdd (f (Additive.toMul a))

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem AddMonoidHom.coe_toMultiplicative' {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) :
                        (AddMonoidHom.toMultiplicative' f) = Multiplicative.ofAdd f Additive.ofMul
                        @[simp]
                        theorem MonoidHom.toAdditive'_symm_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] :
                        ∀ (a : Additive α →+ β) (a_1 : α), (MonoidHom.toAdditive'.symm a) a_1 = Multiplicative.ofAdd (a (Additive.ofMul a_1))
                        @[simp]
                        theorem MonoidHom.toAdditive'_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [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} [MulOneClass α] [AddZeroClass β] :

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

                        Equations
                        • MonoidHom.toAdditive' = AddMonoidHom.toMultiplicative'.symm
                        Instances For
                          @[simp]
                          theorem MonoidHom.coe_toAdditive' {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) :
                          (MonoidHom.toAdditive' f) = Multiplicative.toAdd f Additive.toMul
                          @[simp]
                          theorem AddMonoidHom.toMultiplicative''_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [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} [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) (a : α) :
                          (AddMonoidHom.toMultiplicative''.symm f) a = Additive.ofMul (f (Multiplicative.ofAdd a))

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem AddMonoidHom.coe_toMultiplicative'' {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) :
                            (AddMonoidHom.toMultiplicative'' f) = Additive.toMul f Multiplicative.toAdd
                            @[simp]
                            theorem MonoidHom.toAdditive''_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [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} [AddZeroClass α] [MulOneClass β] :
                            ∀ (a : α →+ Additive β) (a_1 : Multiplicative α), (MonoidHom.toAdditive''.symm a) a_1 = Additive.toMul (a (Multiplicative.toAdd a_1))
                            def MonoidHom.toAdditive'' {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] :

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

                            Equations
                            • MonoidHom.toAdditive'' = AddMonoidHom.toMultiplicative''.symm
                            Instances For
                              @[simp]
                              theorem MonoidHom.coe_toAdditive'' {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) :
                              (MonoidHom.toAdditive'' f) = Additive.ofMul f Multiplicative.ofAdd
                              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
                              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