Documentation

Mathlib.Algebra.Group.Nat.Hom

Extensionality of monoid homs from ℕ #

source
theorem ext_nat' {A : Type u_2} {F : Type u_4} [FunLike F ℕ A] [AddZeroClass A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) :
f = g
source
theorem AddMonoidHom.ext_nat {A : Type u_2} [AddZeroClass A] {f g : ℕ →+ A} :
f 1 = g 1 → f = g
source
theorem AddMonoidHom.ext_nat_iff {A : Type u_2} [AddZeroClass A] {f g : ℕ →+ A} :
f = g ↔ f 1 = g 1
source
def multiplesHom (M : Type u_1) [AddMonoid M] :
M ≃ (ℕ →+ M)

Additive homomorphisms from ℕ are defined by the image of 1.

Equations
    Instances For
      source
      @[simp]
      theorem multiplesHom_apply {M : Type u_1} [AddMonoid M] (x : M) (n : ℕ) :
      ((multiplesHom M) x) n = n • x
      source
      @[simp]
      theorem multiplesHom_symm_apply {M : Type u_1} [AddMonoid M] (f : ℕ →+ M) :
      (multiplesHom M).symm f = f 1
      source
      theorem AddMonoidHom.apply_nat {M : Type u_1} [AddMonoid M] (f : ℕ →+ M) (n : ℕ) :
      f n = n • f 1
      source
      def powersHom (M : Type u_1) [Monoid M] :
      M ≃ (Multiplicative ℕ →* M)

      Monoid homomorphisms from Multiplicative ℕ are defined by the image of Multiplicative.ofAdd 1.

      Equations
        Instances For
          source
          @[simp]
          theorem powersHom_apply {M : Type u_1} [Monoid M] (x : M) (n : Multiplicative ℕ) :
          ((powersHom M) x) n = x ^ Multiplicative.toAdd n
          source
          @[simp]
          theorem powersHom_symm_apply {M : Type u_1} [Monoid M] (f : Multiplicative ℕ →* M) :
          (powersHom M).symm f = f (Multiplicative.ofAdd 1)
          source
          theorem MonoidHom.apply_mnat {M : Type u_1} [Monoid M] (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) :
          f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
          source
          theorem MonoidHom.ext_mnat {M : Type u_1} [Monoid M] ⦃f g : Multiplicative ℕ →* M⦄ (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
          f = g
          source
          theorem MonoidHom.ext_mnat_iff {M : Type u_1} [Monoid M] {f g : Multiplicative ℕ →* M} :
          f = g ↔ f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)
          source
          def multiplesAddHom (M : Type u_1) [AddCommMonoid M] :
          M ≃+ (ℕ →+ M)

          If M is commutative, multiplesHom is an additive equivalence.

          Equations
            Instances For
              source
              @[simp]
              theorem multiplesAddHom_apply {M : Type u_1} [AddCommMonoid M] (x : M) (n : ℕ) :
              ((multiplesAddHom M) x) n = n • x
              source
              @[simp]
              theorem multiplesAddHom_symm_apply {M : Type u_1} [AddCommMonoid M] (f : ℕ →+ M) :
              (multiplesAddHom M).symm f = f 1
              source
              def powersMulHom (M : Type u_1) [CommMonoid M] :
              M ≃* (Multiplicative ℕ →* M)

              If M is commutative, powersHom is a multiplicative equivalence.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem powersMulHom_apply {M : Type u_1} [CommMonoid M] (x : M) (n : Multiplicative ℕ) :
                  ((powersMulHom M) x) n = x ^ Multiplicative.toAdd n
                  source
                  @[simp]
                  theorem powersMulHom_symm_apply {M : Type u_1} [CommMonoid M] (f : Multiplicative ℕ →* M) :
                  (powersMulHom M).symm f = f (Multiplicative.ofAdd 1)