liftNC_one — Mathlib

English

For any f: k →+* R and any g of the appropriate fashion, the liftNC map sends the unit of the source algebra to the unit of R; i.e., liftNC f g 1 = 1.

Русский

Для любого отображения f: k →+* R и любого g соответствующего типа отображения, отображение liftNC отправляет единицу исходной алгебры в единицу пространства целевого кольца: liftNC f g 1 = 1.

LaTeX

$$$ liftNC (f : k \to+ R) g \; 1 = 1 $$$

Lean4

@[simp]
theorem liftNC_one {g_hom R : Type*} [NonAssocSemiring k] [One G] [Semiring R] [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 only [one_def, liftNC_single, AddMonoidHom.coe_coe, map_one, mul_one]

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