lift — Mathlib

English

The equivalence IsFreeGroup.lift is the canonical correspondence between generator functions and group homomorphisms.

Русский

Эквивелентность IsFreeGroup.lift задаёт каноническую соответствие между функциями-генераторами и гомоморфизмами группы.

LaTeX

$$lift : (Generators G → H) ≃ (G →* H)$$

Lean4

/-- The equivalence between functions on the generators and group homomorphisms from a free group
given by those generators. -/
def lift : (Generators G → H) ≃ (G →* H) :=
  (basis G).lift

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