Documentation

Mathlib.Algebra.Group.Equiv.TypeTags

Additive and multiplicative equivalences associated to Multiplicative and Additive. #

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

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

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

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

            Equations
            • MulEquiv.toAdditive'' = AddEquiv.toMultiplicative''.symm
            Instances For
              source
              @[simp]
              theorem monoidEndToAdditive_apply (M : Type u_3) [MulOneClass M] :
              ∀ (a : M →* M), (monoidEndToAdditive M) a = Equiv.toFun MonoidHom.toAdditive a
              source
              @[simp]
              theorem monoidEndToAdditive_symm_apply (M : Type u_3) [MulOneClass M] :
              ∀ (a : Additive M →+ Additive M), (MulEquiv.symm (monoidEndToAdditive M)) a = Equiv.invFun MonoidHom.toAdditive a
              source
              def monoidEndToAdditive (M : Type u_3) [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
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem addMonoidEndToMultiplicative_symm_apply (A : Type u_3) [AddZeroClass A] :
                ∀ (a : Multiplicative A →* Multiplicative A), (MulEquiv.symm (addMonoidEndToMultiplicative A)) a = Equiv.invFun AddMonoidHom.toMultiplicative a
                source
                @[simp]
                theorem addMonoidEndToMultiplicative_apply (A : Type u_3) [AddZeroClass A] :
                ∀ (a : A →+ A), (addMonoidEndToMultiplicative A) a = Equiv.toFun AddMonoidHom.toMultiplicative a
                source
                def addMonoidEndToMultiplicative (A : Type u_3) [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
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem AddEquiv.additiveMultiplicative_symm_apply (G : Type u_1) [AddZeroClass G] (a : G) :
                  (AddEquiv.symm (AddEquiv.additiveMultiplicative G)) a = Additive.ofMul (Multiplicative.ofAdd a)
                  source
                  @[simp]
                  theorem AddEquiv.additiveMultiplicative_apply (G : Type u_1) [AddZeroClass G] (a : Additive (Multiplicative G)) :
                  (AddEquiv.additiveMultiplicative G) a = Multiplicative.toAdd (Additive.toMul a)
                  source
                  def AddEquiv.additiveMultiplicative (G : Type u_1) [AddZeroClass G] :
                  Additive (Multiplicative G) ≃+ G

                  Additive (Multiplicative G) is just G.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem MulEquiv.multiplicativeAdditive_symm_apply (H : Type u_2) [MulOneClass H] (a : H) :
                    (MulEquiv.symm (MulEquiv.multiplicativeAdditive H)) a = Multiplicative.ofAdd (Additive.ofMul a)
                    source
                    @[simp]
                    theorem MulEquiv.multiplicativeAdditive_apply (H : Type u_2) [MulOneClass H] (a : Multiplicative (Additive H)) :
                    (MulEquiv.multiplicativeAdditive H) a = Additive.toMul (Multiplicative.toAdd a)
                    source
                    def MulEquiv.multiplicativeAdditive (H : Type u_2) [MulOneClass H] :
                    Multiplicative (Additive H) ≃* H

                    Multiplicative (Additive H) is just H.

                    Equations
                    Instances For