freeMk — Mathlib

English

An element of the free R-module on X is represented by a finite sum of basis elements corresponding to generators x ∈ X, encoded as a single function sending each generator to its coefficient.

Русский

Элемент свободного R-модуля над X задаётся как конечная сумма базисных элементов, соответствующих генераторам x ∈ X, с коэффициентами.

LaTeX

$$$\text{freeMk}: X \to (\mathrm{Free}(R)).obj X$ is given by $x \mapsto \text{basis}_{x}$, i.e., $\mathrm{freeMk}(x) = \delta_x$.$$

Lean4

/-- Constructor for elements in the module `(free R).obj X`. -/
noncomputable def freeMk {X : Type u} (x : X) : (free R).obj X :=
  Finsupp.single x 1

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