finsupp — Mathlib

English

From a presentation of a module N, one obtains the obvious presentation of the free module ι →0 N; i.e., the basis indexed by ι with no relations, transported along the finsupp equivalence.

Русский

Из презентации модуля N получается очевидная презентация свободного модуля ι →0 N; базис индексируемый по ι без отношений, перенесённых через эквивалентность finsupp.

LaTeX

$$$\\text{Module.Presentation.finsupp} : \\text{Presentation } A(ι\\to_0 N)$$$

Lean4

/-- The obvious presentation of the module `ι →₀ N` that is deduced from a presentation
of the module `N`. -/
@[simps! G R relation]
noncomputable def finsupp : Presentation A (ι →₀ N) :=
  (directSum (fun (_ : ι) ↦ pres)).ofLinearEquiv (finsuppLequivDFinsupp _).symm

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