coe_coe

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coe_coe

English

Duplicate of 196407: the coercion to semilinear maps is injective.

Русский

Дублирует 196407: приведение к семилинейным отображениям инъективно.

LaTeX

$$$(f : M_1 \toSL[\sigma_{12}] M_2) = g \Leftrightarrow f = g$$$

Lean4

@[simp, norm_cast]
theorem coe_coe (f : M₁ →SL[σ₁₂] M₂) : ⇑(f : M₁ →ₛₗ[σ₁₂] M₂) = f :=
  rfl

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

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

Разделы

Аффилиация

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