coe_semilinearMap

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.coe_semilinearMap

English

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

Русский

Базовая функция f, рассматриваемая как семилинейное отображение, равна самому f.

LaTeX

$$$((f : M \to_\sigma M_3) : M \to M_3) = f$$$

Lean4

theorem coe_semilinearMap {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :
    ((f : M →ₛₗ[σ] M₃) : M → M₃) = f :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru