free_map_apply — Mathlib

English

For a map f: X → Y, the induced map on free modules takes the generator corresponding to x to the generator of f(x).

Русский

Для отображения f: X → Y получаем отображение свободных модулей, которое отправляет свободный элемент x на свободный элемент f(x).

LaTeX

$$$\mathrm{free}(R).map f(\mathrm{freeMk}(x)) = \mathrm{freeMk}(f(x))$$$

Lean4

@[simp]
theorem free_map_apply {X Y : Type u} (f : X → Y) (x : X) : (free R).map f (freeMk x) = freeMk (f x) := by
  apply Finsupp.mapDomain_single

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