Documentation

Mathlib.Algebra.Group.Equiv.TypeTags

Additive and multiplicative equivalences associated to Multiplicative and Additive. #

source
def AddEquiv.toMultiplicative {G : Type u_2} {H : Type u_3} [AddZeroClass G] [AddZeroClass 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.
Instances For
    source
    @[simp]
    theorem AddEquiv.toMultiplicative_apply_symm_apply {G : Type u_2} {H : Type u_3} [AddZeroClass G] [AddZeroClass H] (f : G ≃+ H) (a : Multiplicative H) :
    (toMultiplicative f).symm a = (AddMonoidHom.toMultiplicative f.symm.toAddMonoidHom) a
    source
    @[simp]
    theorem AddEquiv.toMultiplicative_symm_apply_symm_apply {G : Type u_2} {H : Type u_3} [AddZeroClass G] [AddZeroClass H] (f : Multiplicative G ≃* Multiplicative H) (a : H) :
    (toMultiplicative.symm f).symm a = (AddMonoidHom.toMultiplicative.symm f.symm.toMonoidHom) a
    source
    @[simp]
    theorem AddEquiv.toMultiplicative_apply_apply {G : Type u_2} {H : Type u_3} [AddZeroClass G] [AddZeroClass H] (f : G ≃+ H) (a : Multiplicative G) :
    (toMultiplicative f) a = (AddMonoidHom.toMultiplicative f.toAddMonoidHom) a
    source
    @[simp]
    theorem AddEquiv.toMultiplicative_symm_apply_apply {G : Type u_2} {H : Type u_3} [AddZeroClass G] [AddZeroClass H] (f : Multiplicative G ≃* Multiplicative H) (a : G) :
    (toMultiplicative.symm f) a = (AddMonoidHom.toMultiplicative.symm f.toMonoidHom) a
    source
    def MulEquiv.toAdditive {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass 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.
    Instances For
      source
      @[simp]
      theorem MulEquiv.toAdditive_apply_symm_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass H] (f : G ≃* H) (a : Additive H) :
      (toAdditive f).symm a = (MonoidHom.toAdditive f.symm.toMonoidHom) a
      source
      @[simp]
      theorem MulEquiv.toAdditive_symm_apply_symm_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass H] (f : Additive G ≃+ Additive H) (a : H) :
      (toAdditive.symm f).symm a = (MonoidHom.toAdditive.symm f.symm.toAddMonoidHom) a
      source
      @[simp]
      theorem MulEquiv.toAdditive_apply_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass H] (f : G ≃* H) (a : Additive G) :
      (toAdditive f) a = (MonoidHom.toAdditive f.toMonoidHom) a
      source
      @[simp]
      theorem MulEquiv.toAdditive_symm_apply_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass H] (f : Additive G ≃+ Additive H) (a : G) :
      (toAdditive.symm f) a = (MonoidHom.toAdditive.symm f.toAddMonoidHom) a
      source
      def AddEquiv.toMultiplicative' {G : Type u_2} {H : Type u_3} [MulOneClass G] [AddZeroClass 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.
      Instances For
        source
        @[simp]
        theorem AddEquiv.toMultiplicative'_apply_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [AddZeroClass H] (f : Additive G ≃+ H) (a : G) :
        (toMultiplicative' f) a = (AddMonoidHom.toMultiplicative' f.toAddMonoidHom) a
        source
        @[simp]
        theorem AddEquiv.toMultiplicative'_symm_apply_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [AddZeroClass H] (f : G ≃* Multiplicative H) (a : Additive G) :
        (toMultiplicative'.symm f) a = (AddMonoidHom.toMultiplicative'.symm f.toMonoidHom) a
        source
        @[simp]
        theorem AddEquiv.toMultiplicative'_symm_apply_symm_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [AddZeroClass H] (f : G ≃* Multiplicative H) (a : H) :
        (toMultiplicative'.symm f).symm a = (AddMonoidHom.toMultiplicative''.symm f.symm.toMonoidHom) a
        source
        @[simp]
        theorem AddEquiv.toMultiplicative'_apply_symm_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [AddZeroClass H] (f : Additive G ≃+ H) (a : Multiplicative H) :
        (toMultiplicative' f).symm a = (AddMonoidHom.toMultiplicative'' f.symm.toAddMonoidHom) a
        source
        @[reducible, inline]
        abbrev MulEquiv.toAdditive' {G : Type u_2} {H : Type u_3} [MulOneClass G] [AddZeroClass H] :
        G ≃* Multiplicative H ≃ (Additive G ≃+ H)

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

        Equations
        Instances For
          source
          def AddEquiv.toMultiplicative'' {G : Type u_2} {H : Type u_3} [AddZeroClass G] [MulOneClass 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.
          Instances For
            source
            @[simp]
            theorem AddEquiv.toMultiplicative''_apply_apply {G : Type u_2} {H : Type u_3} [AddZeroClass G] [MulOneClass H] (f : G ≃+ Additive H) (a : Multiplicative G) :
            (toMultiplicative'' f) a = (AddMonoidHom.toMultiplicative'' f.toAddMonoidHom) a
            source
            @[simp]
            theorem AddEquiv.toMultiplicative''_symm_apply_symm_apply {G : Type u_2} {H : Type u_3} [AddZeroClass G] [MulOneClass H] (f : Multiplicative G ≃* H) (a : Additive H) :
            (toMultiplicative''.symm f).symm a = (AddMonoidHom.toMultiplicative'.symm f.symm.toMonoidHom) a
            source
            @[simp]
            theorem AddEquiv.toMultiplicative''_symm_apply_apply {G : Type u_2} {H : Type u_3} [AddZeroClass G] [MulOneClass H] (f : Multiplicative G ≃* H) (a : G) :
            (toMultiplicative''.symm f) a = (AddMonoidHom.toMultiplicative''.symm f.toMonoidHom) a
            source
            @[simp]
            theorem AddEquiv.toMultiplicative''_apply_symm_apply {G : Type u_2} {H : Type u_3} [AddZeroClass G] [MulOneClass H] (f : G ≃+ Additive H) (a : H) :
            (toMultiplicative'' f).symm a = (AddMonoidHom.toMultiplicative' f.symm.toAddMonoidHom) a
            source
            @[reducible, inline]
            abbrev MulEquiv.toAdditive'' {G : Type u_2} {H : Type u_3} [AddZeroClass G] [MulOneClass H] :
            Multiplicative G ≃* H ≃ (G ≃+ Additive H)

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

            Equations
            Instances For
              source
              def MulEquiv.toMultiplicative_toAdditive {G : Type u_2} [MulOneClass G] :
              Multiplicative (Additive G) ≃* G

              The multiplicative version of an additivized monoid is mul-equivalent to itself.

              Equations
              Instances For
                source
                @[simp]
                theorem MulEquiv.toMultiplicative_toAdditive_symm_apply {G : Type u_2} [MulOneClass G] (a : G) :
                toMultiplicative_toAdditive.symm a = Multiplicative.ofAdd (Additive.ofMul a)
                source
                @[simp]
                theorem MulEquiv.toMultiplicative_toAdditive_apply {G : Type u_2} [MulOneClass G] (a : Multiplicative (Additive G)) :
                toMultiplicative_toAdditive a = Additive.toMul (Multiplicative.toAdd a)
                source
                def AddEquiv.toAdditive_toMultiplicative {G : Type u_2} [AddZeroClass G] :
                Additive (Multiplicative G) ≃+ G

                The additive version of an multiplicativized additive monoid is add-equivalent to itself.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem AddEquiv.toAdditive_toMultiplicative_symm_apply {G : Type u_2} [AddZeroClass G] (a : G) :
                  toAdditive_toMultiplicative.symm a = Additive.ofMul (Multiplicative.ofAdd a)
                  source
                  @[simp]
                  theorem AddEquiv.toAdditive_toMultiplicative_apply {G : Type u_2} [AddZeroClass G] (a : Additive (Multiplicative G)) :
                  toAdditive_toMultiplicative a = Multiplicative.toAdd (Additive.toMul a)
                  source
                  def monoidEndToAdditive (M : Type u_4) [MulOneClass M] :
                  Monoid.End M ≃* AddMonoid.End (Additive M)

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

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem monoidEndToAdditive_apply_apply (M : Type u_4) [MulOneClass M] (f : M →* M) (a : Additive M) :
                    ((monoidEndToAdditive M) f) a = Additive.ofMul (f (Additive.toMul a))
                    source
                    @[simp]
                    theorem monoidEndToAdditive_symm_apply_apply (M : Type u_4) [MulOneClass M] (f : Additive M →+ Additive M) (a : M) :
                    ((monoidEndToAdditive M).symm f) a = Additive.toMul (f (Additive.ofMul a))
                    source
                    def addMonoidEndToMultiplicative (A : Type u_4) [AddZeroClass A] :
                    AddMonoid.End A ≃* Monoid.End (Multiplicative A)

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

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem addMonoidEndToMultiplicative_symm_apply_apply (A : Type u_4) [AddZeroClass A] (f : Multiplicative A →* Multiplicative A) (a : A) :
                      ((addMonoidEndToMultiplicative A).symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))
                      source
                      @[simp]
                      theorem addMonoidEndToMultiplicative_apply_apply (A : Type u_4) [AddZeroClass A] (f : A →+ A) (a : Multiplicative A) :
                      ((addMonoidEndToMultiplicative A) f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))
                      source
                      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.
                      Instances For
                        source
                        @[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)
                        source
                        @[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)
                        source
                        @[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
                        Instances For
                          source
                          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.
                          Instances For
                            source
                            @[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)
                            source
                            @[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)
                            source
                            @[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
                            Instances For
                              source
                              def AddEquiv.additiveMultiplicative (G : Type u_2) [AddZeroClass G] :
                              Additive (Multiplicative G) ≃+ G

                              Additive (Multiplicative G) is just G.

                              Equations
                              Instances For
                                source
                                @[simp]
                                theorem AddEquiv.additiveMultiplicative_apply (G : Type u_2) [AddZeroClass G] (a : Additive (Multiplicative G)) :
                                (additiveMultiplicative G) a = Multiplicative.toAdd (Additive.toMul a)
                                source
                                @[simp]
                                theorem AddEquiv.additiveMultiplicative_symm_apply (G : Type u_2) [AddZeroClass G] (a : G) :
                                (additiveMultiplicative G).symm a = Additive.ofMul (Multiplicative.ofAdd a)
                                source
                                def MulEquiv.multiplicativeAdditive (H : Type u_3) [MulOneClass H] :
                                Multiplicative (Additive H) ≃* H

                                Multiplicative (Additive H) is just H.

                                Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem MulEquiv.multiplicativeAdditive_symm_apply (H : Type u_3) [MulOneClass H] (a : H) :
                                  (multiplicativeAdditive H).symm a = Multiplicative.ofAdd (Additive.ofMul a)
                                  source
                                  @[simp]
                                  theorem MulEquiv.multiplicativeAdditive_apply (H : Type u_3) [MulOneClass H] (a : Multiplicative (Additive H)) :
                                  (multiplicativeAdditive H) a = Additive.toMul (Multiplicative.toAdd a)
                                  source
                                  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.
                                  Instances For
                                    source
                                    @[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)
                                    source
                                    @[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)
                                    source
                                    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.
                                    Instances For
                                      source
                                      @[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)
                                      source
                                      @[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)
                                      source
                                      def MulEquiv.Monoid.End {M : Type u_4} [Monoid M] :
                                      _root_.Monoid.End M ≃* _root_.AddMonoid.End (Additive M)

                                      Monoid.End M is equivalent to AddMonoid.End (Additive M).

                                      Equations
                                      Instances For
                                        source
                                        @[simp]
                                        theorem MulEquiv.Monoid.End_apply {M : Type u_4} [Monoid M] (f : M →* M) :
                                        End f = { toFun := fun (a : Additive M) => Additive.ofMul (f (Additive.toMul a)), map_zero' := ⋯, map_add' := ⋯ }
                                        source
                                        def MulEquiv.AddMonoid.End {M : Type u_4} [AddMonoid M] :
                                        _root_.AddMonoid.End M ≃* _root_.Monoid.End (Multiplicative M)

                                        AddMonoid.End M is equivalent to Monoid.End (Multiplicative M).

                                        Equations
                                        Instances For
                                          source
                                          @[simp]
                                          theorem MulEquiv.AddMonoid.End_apply {M : Type u_4} [AddMonoid M] (f : M →+ M) :
                                          End f = { toFun := fun (a : Multiplicative M) => Multiplicative.ofAdd (f (Multiplicative.toAdd a)), map_one' := ⋯, map_mul' := ⋯ }