dual_zero

Mathlib.Algebra.Module.CharacterModule

URI: https://scilib.ai/kg/mathlib#CharacterModule.dual_zero

English

The dual of the zero linear map is the zero in the dual space: dual(0) = 0.

Русский

Дуальное отображение нулевой карты равно нулю в дуальном пространстве: dual(0) = 0.

LaTeX

$$$\mathrm{dual}(0) = 0$$$

Lean4

@[simp]
theorem dual_zero : dual (0 : A →ₗ[R] B) = 0 := by
  ext f
  exact map_zero f

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

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

Разделы

Аффилиация

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