Documentation

Mathlib.Algebra.Group.Equiv.TypeTags

Additive and multiplicative equivalences associated to Multiplicative and Additive. #

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def MulEquiv.toAdditive {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass H] :

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem MulEquiv.toAdditive_apply_apply {G : Type u_2} {H : Type u_3} [MulOneClass G] [MulOneClass H] (f : G ≃* H) (a : Additive G) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[reducible, inline]

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

        Equations
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible, inline]

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

            Equations
            Instances For

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

              Equations
              Instances For
                @[simp]

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

                Equations
                Instances For
                  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
                    @[simp]
                    theorem MulEquiv.piMultiplicative_symm_apply {ι : Type u_1} (K : ιType u_4) [(i : ι) → Add (K i)] (x : (i : ι) → Multiplicative (K i)) :
                    @[simp]
                    theorem MulEquiv.piMultiplicative_apply {ι : Type u_1} (K : ιType u_4) [(i : ι) → Add (K i)] (x : Multiplicative ((i : ι) → K i)) (i : ι) :
                    @[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
                      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
                        @[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)
                        @[simp]
                        theorem AddEquiv.piAdditive_apply {ι : Type u_1} (K : ιType u_4) [(i : ι) → Mul (K i)] (x : Additive ((i : ι) → K i)) (i : ι) :
                        @[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

                          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
                            def AddEquiv.prodAdditive (G : Type u_2) (H : Type u_3) [Mul G] [Mul 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
                              @[simp]
                              @[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)