Documentation

Mathlib.Algebra.Module.ZMod

The ZMod n-module structure on Abelian groups whose elements have order dividing n #

@[reducible, inline]
abbrev AddCommMonoid.zmodModule {n : } {M : Type u_1} [NeZero n] [AddCommMonoid M] (h : ∀ (x : M), n x = 0) :
Module (ZMod n) M

The ZMod n-module structure on commutative monoids whose elements have order dividing n ≠ 0. Also implies a group structure via Module.addCommMonoidToAddCommGroup. See note [reducible non-instances].

Equations
Instances For
    @[reducible, inline]
    abbrev AddCommGroup.zmodModule {n : } {G : Type u_3} [AddCommGroup G] (h : ∀ (x : G), n x = 0) :
    Module (ZMod n) G

    The ZMod n-module structure on Abelian groups whose elements have order dividing n. See note [reducible non-instances].

    Equations
    Instances For
      theorem ZMod.map_smul {n : } {M : Type u_1} {M₁ : Type u_2} {F : Type u_3} [AddCommGroup M] [AddCommGroup M₁] [FunLike F M M₁] [AddMonoidHomClass F M M₁] [Module (ZMod n) M] [Module (ZMod n) M₁] (f : F) (c : ZMod n) (x : M) :
      f (c x) = c f x
      theorem ZMod.smul_mem {n : } {M : Type u_1} {S : Type u_4} [AddCommGroup M] [Module (ZMod n) M] [SetLike S M] [AddSubgroupClass S M] {x : M} {K : S} (hx : x K) (c : ZMod n) :
      c x K
      def AddMonoidHom.toZModLinearMap (n : ) {M : Type u_1} {M₁ : Type u_2} [AddCommGroup M] [AddCommGroup M₁] [Module (ZMod n) M] [Module (ZMod n) M₁] (f : M →+ M₁) :
      M →ₗ[ZMod n] M₁

      Reinterpret an additive homomorphism as a ℤ/nℤ-linear map.

      See also: AddMonoidHom.toIntLinearMap, AddMonoidHom.toNatLinearMap, AddMonoidHom.toRatLinearMap

      Equations
      Instances For
        @[simp]
        theorem AddMonoidHom.coe_toZModLinearMap (n : ) {M : Type u_1} {M₁ : Type u_2} [AddCommGroup M] [AddCommGroup M₁] [Module (ZMod n) M] [Module (ZMod n) M₁] (f : M →+ M₁) :

        Reinterpret an additive subgroup of a ℤ/nℤ-module as a ℤ/nℤ-submodule.

        See also: AddSubgroup.toIntSubmodule, AddSubmonoid.toNatSubmodule.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem AddSubgroup.toZModSubmodule_symm (n : ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] :
          (AddSubgroup.toZModSubmodule n).symm = Submodule.toAddSubgroup
          @[simp]
          theorem AddSubgroup.coe_toZModSubmodule (n : ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : AddSubgroup M) :
          @[simp]
          theorem AddSubgroup.mem_toZModSubmodule (n : ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] {x : M} {S : AddSubgroup M} :
          @[simp]
          theorem AddSubgroup.toZModSubmodule_toAddSubgroup (n : ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : AddSubgroup M) :
          ((AddSubgroup.toZModSubmodule n) S).toAddSubgroup = S
          @[simp]
          theorem Submodule.toAddSubgroup_toZModSubmodule (n : ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : Submodule (ZMod n) M) :
          (AddSubgroup.toZModSubmodule n) S.toAddSubgroup = S