zmodModule — Mathlib

English

For a given n ≠ 0 and an additive commutative monoid M in which n·x = 0 for all x, one can endow M with a module structure over ZMod n via the natural action.

Русский

Если n ≠ 0 и у моноида M выполняется n·x = 0 для всех x, то на M можно надстроить структуру модуля над ZMod n через естественное действие.

LaTeX

$$$\\text{zmodModule}(M, n, h) : M \\text{ becomes a } \\mathbb{Z}/n\\mathbb{Z}\\text{-module}$$$

Lean4

/-- 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]. -/
abbrev zmodModule [NeZero n] [AddCommMonoid M] (h : ∀ (x : M), n • x = 0) : Module (ZMod n) M :=
  by
  have h_mod (c : ℕ) (x : M) : (c % n) • x = c • x :=
    by
    suffices (c % n + c / n * n) • x = c • x by rwa [add_nsmul, mul_nsmul, h, add_zero] at this
    rw [Nat.mod_add_div']
  have := NeZero.ne n
  match n with
  | n + 1 =>
    exact
      { smul := fun (c : Fin _) x ↦ c.val • x
        smul_zero := fun _ ↦ nsmul_zero _
        zero_smul := fun _ ↦ zero_nsmul _
        smul_add := fun _ _ _ ↦ nsmul_add _ _ _
        one_smul := fun _ ↦ (h_mod _ _).trans <| one_nsmul _
        add_smul := fun _ _ _ ↦ (h_mod _ _).trans <| add_nsmul _ _ _
        mul_smul := fun _ _ _ ↦ (h_mod _ _).trans <| mul_nsmul' _ _ _ }

Похожие утверждения