coe_coe — Mathlib

English

For any coalgebra equivalence e, the coercion to a linear map equals e itself viewed as a linear map; i.e., the underlying map is exactly e.

Русский

Для любой коалгебраической эквивалентности e приведение к линейному отображению совпадает с самим e, рассматриваемым как линейное отображение.

LaTeX

$$$ (e : A \\simeq_{\\ell_c[R]} B) \\to (A \\to_{\\ell_c[R]} B) = e$$$

Lean4

@[simp, norm_cast]
theorem coe_coe : ⇑(e : A →ₗc[R] B) = e :=
  rfl

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