coe_mk — Mathlib

English

A simp lemma that reduces equality of ContinuousAlgHom to equality of underlying functions.

Русский

Лемма упрощения, которая сводит равенство ContinuousAlgHom к равенству соответствующих функций.

LaTeX

$$$f,g:\\text{ContinuousAlgHom}\\ R\\ A\\ B, (f = g) \\Leftrightarrow (\\text{underlying function of } f = \\text{underlying function of } g)$$$

Lean4

@[simp]
theorem coe_mk (f : A →ₐ[R] B) (h) : (mk f h : A →ₐ[R] B) = f :=
  rfl

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