instNontrivialDual

Mathlib.LinearAlgebra.Dual.Lemmas

URI: https://scilib.ai/kg/mathlib#Module.instNontrivialDual

English

If V is nontrivial, then its dual is nontrivial.

Русский

Если V не тривиально, то и его двойственный модуль не тривиален.

LaTeX

$$Nontrivial($V$) $\\Rightarrow$ Nontrivial($V^{\\ast}$)$$

Lean4

instance instNontrivialDual [Nontrivial V] : Nontrivial (Dual K V) :=
  (nontrivial_dual_iff K).mpr inferInstance

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

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

Разделы

Аффилиация

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