lift_of — Mathlib

English

Let F: G →* A be a monoid homomorphism. Then lift k G A F applied to the image of x under the embedding of G into MonoidAlgebra, namely of k G x, equals F(x): lift k G A F (of k G x) = F x.

Русский

Пусть F: G →* A – гомоморфизм моноидов. Тогда lift k G A F на образе x через вложение of k Gx равен F(x): lift k G A F (of k G x) = F x.

LaTeX

$$$\\mathrm{lift}_{k,G,A}(F)(\\mathrm{of}_{k,G}(x)) = F(x).$$$

Lean4

theorem lift_of (F : G →* A) (x) : lift k G A F (of k G x) = F x := by simp

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