zero_notMem_image

Mathlib.LinearAlgebra.LinearIndependent.Defs

URI: https://scilib.ai/kg/mathlib#LinearIndepOn.zero_notMem_image

English

If LinearIndepOn R v s holds, then 0 is not in the image of v restricted to s.

Русский

Если LinearIndepOn R v s, то 0 не лежит в образе v на s.

LaTeX

$$$[\\Nontrivial R] (hv : LinearIndepOn R v s) \\Rightarrow 0 \\notin v''s$$$

Lean4

theorem zero_notMem_image [Nontrivial R] (hs : LinearIndepOn R v s) : 0 ∉ v '' s := fun ⟨_, hi, h0⟩ ↦ hs.ne_zero hi h0

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

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

Разделы

Аффилиация

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