coe_coe — Mathlib

English

The underlying function of f viewed as a semilinear map is just f itself.

Русский

Функциональная часть отображения f, рассматриваемого как семилинейное отображение, равна самому f.

LaTeX

$$$\big(\,f : M \to_\sll[\sigma] M_3\,\big) : M \to M_3 = f$$$

Lean4

@[simp, norm_cast]
theorem coe_coe {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} : ⇑(f : M →ₛₗ[σ] M₃) = f :=
  rfl

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