coe_liftNCAlgHom — Mathlib

English

The coercion of the liftNCAlgHom equals liftNC; i.e., the underlying function of liftNCAlgHom matches the canonical liftNC construction.

Русский

Сведение liftNCAlgHom к функции совпадает с канонической конструкцией liftNC.

LaTeX

$$$ \\big( \\mathrm{coe}\\_{{AddMonoidAlgebra}}(\\mathrm{liftNCAlgHom}\\ f\\ g\\ h) \\big) = \\mathrm{liftNC}\\ f\\ g $$$

Lean4

@[simp]
theorem coe_liftNCAlgHom (f : A →ₐ[k] B) (g : Multiplicative G →* B) (h_comm) :
    ⇑(liftNCAlgHom f g h_comm) = liftNC f g :=
  rfl

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