coe_coe — Mathlib

English

The coe_coe theorem asserts the equality of the funLike.coe and the underlying coe for AlgHom within AlgHomClass.

Русский

Теорема coe_coe утверждает равенство функций funLike.coe и базового преобразования для AlgHom внутри AlgHomClass.

LaTeX

$$$\\text{AlgHom.funLike.coe}(\\text{toAlgHom } f) = \\text{coeff}(f)$$$

Lean4

@[simp]
protected theorem coe_coe {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : ⇑(f : A →ₐ[R] B) = f :=
  rfl

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