toZModLinearMap — Mathlib

English

The conversion between AddMonoidHom and ZMod-linear maps is itself an equivalence.

Русский

Переобразование между AddMonoidHom и ZMod-линейными отображениями является эквивалентностью.

LaTeX

$$$\\text{toZModLinearMapEquiv} : (M \\to_+ M_1) \\simeq_+ (M \\to_\\ell[ZMod n] M_1)$$$

Lean4

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

See also:
`AddMonoidHom.toIntLinearMap`, `AddMonoidHom.toNatLinearMap`, `AddMonoidHom.toRatLinearMap` -/
def toZModLinearMap (f : M →+ M₁) : M →ₗ[ZMod n] M₁ :=
  { f with map_smul' := ZMod.map_smul f }

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