toZModLinearMapEquiv — Mathlib

English

The equivalence preserves addition: the forward and inverse maps respect addition of homomorphisms.

Русский

Эквивалентность сохраняет сложение: переходы вперёд и назад сохраняют сложение гомоморфизмов.

LaTeX

$$$\\text{toZModLinearMapEquiv}(f_1+f_2) = \\text{toZModLinearMapEquiv}(f_1) + \\text{toZModLinearMapEquiv}(f_2)$$$

Lean4

/-- `AddMonoidHom.toZModLinearMap` as an equivalence. -/
def toZModLinearMapEquiv : (M →+ M₁) ≃+ (M →ₗ[ZMod n] M₁)
    where
  toFun f := f.toZModLinearMap n
  invFun g := g
  map_add' f₁ f₂ := by ext; simp

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