liftNC_one — Mathlib

English

Let f be a ring hom and g a one-homomorphism. Then liftNC (f) g sends the unit 1 to 1: liftNC (f) g 1 = 1.

Русский

Пусть f — кольцевой гомоморфизм и g — единичный гомоморфизм. Тогда liftNC (f) g отображает единицу в единицу: liftNC (f) g 1 = 1.

LaTeX

$$$ liftNC (f) g (1) = 1 $$$

Lean4

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

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