lift_symm_apply — Mathlib

English

For any f, lift.symm f = f ∘ of; i.e., the symm side recovers f by precomposing with the projection.

Русский

Для любого f, lift.symm f = f ∘ of; т.е. симметрическая часть восстанавливает f посредством предсложения через проекцию.

LaTeX

$$$$ \\mathrm{lift.symm}(f) = f \\circ \\mathrm{of}. $$$$

Lean4

@[simp]
theorem lift_symm_apply (f : Abelianization G →* A) : lift.symm f = f.comp of :=
  rfl

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