instFreeInt — Mathlib

English

There is a free module structure over Z on FreeAbelianGroup σ; a basis exists given by the equivalence with finsupp.

Русский

У FreeAbelianGroup σ имеется свободная структура над Z; база задаётся эквиваленцией с Finsupp.

LaTeX

$$$\\text{Module.Free } \\mathbb{Z}\\; (\\text{FreeAbelianGroup } \\sigma)$$$

Lean4

instance {σ : Type*} : Module.Free ℤ (FreeAbelianGroup σ) where
  exists_basis := ⟨σ, ⟨(FreeAbelianGroup.equivFinsupp _).toIntLinearEquiv⟩⟩

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