liftNC_one — Mathlib

English

The liftNC construction sends the unit 1 of the base ring to the unit of the target monoid algebra.

Русский

Конструкция liftNC отображает единицу базовой кольца в единицу целевой моноидной Алгебры.

LaTeX

$$$liftNC\ f\ g\ 1 = 1$$$

Lean4

@[simp]
theorem liftNC_one {g_hom : Type*} [FunLike g_hom G R] [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom) :
    liftNC (f : k →+ R) g 1 = 1 := by simp [one_def]

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