freeAb — Mathlib

English

There is a functor assigning to every condensed set its free condensed abelian group; this functor is from CondensedSet to CondensedAb.

Русский

Существует функтор, ставящий конденсированное множество в свободную конденсированную абелеву группу; этот функтор идёт из CondensedSet в CondensedAb.

LaTeX

$$$\mathrm{freeAb} : \mathrm{CondensedSet} \to \mathrm{CondensedAb}$$$

Lean4

/-- The free condensed abelian group on a condensed set. -/
noncomputable abbrev freeAb : CondensedSet ⥤ CondensedAb :=
  free _

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