FGModuleCatDual_coe

Mathlib.Algebra.Category.FGModuleCat.Basic

URI: https://scilib.ai/kg/mathlib#FGModuleCat.FGModuleCatDual_coe

English

The carrier of FGModuleCatDual K V coincides with the standard dual module V^* = Module.Dual K V.

Русский

носитель FGModuleCatDual K V совпадает с обычным двойственным модулем V^* = Module.Dual K V.

LaTeX

$$$(FGModuleCatDual\ K\ V).\mathrm{carrier} = Module.Dual\ K\ V$$$

Lean4

@[simp]
theorem FGModuleCatDual_coe : (FGModuleCatDual K V : Type u) = Module.Dual K V :=
  rfl

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

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

Разделы

Аффилиация

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