addMonoidHom — Mathlib

English

There is a free ℤ-structure on M →+ N compatible with the free linear map space.

Русский

Существует свободная структура ℤ на отображениях M →+ N совместимая с пространством линейных отображений.

LaTeX

$$$$ \text{Free}(\mathbb{Z}, M \to+ N) $$$$

Lean4

instance addMonoidHom [Module.Free ℤ N] : Module.Free ℤ (M →+ N) :=
  letI : Module.Free ℤ (M →ₗ[ℤ] N) := Module.Free.linearMap _ _ _ _
  Module.Free.of_equiv (addMonoidHomLequivInt ℤ).symm

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