lift_comp_of' — Mathlib

English

Lifts a magma homomorphism on α to a semigroup homomorphism on the quotient Magma.AssocQuotient α.

Русский

Поднимает морфизм магмы α в семигруппоморфизм над квази-однородной частью Magma.AssocQuotient α.

LaTeX

$$$\mathrm{lift} : (\alpha \to_{\mathsf{n}*} \beta) \simeq (\mathrm{AssocQuotient}(\alpha) \to_{\mathsf{n}*} \beta)$$$

Lean4

@[to_additive (attr := simp)]
theorem lift_comp_of' (f : FreeMagma α →ₙ* β) : lift (f ∘ of) = f :=
  lift.apply_symm_apply f

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