id_image

Mathlib.LinearAlgebra.LinearIndependent.Basic

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

English

If v is linearly independent and w maps indices to units, then w • v is linearly independent.

Русский

Если v линейно независимо и w отображает индексы в единицы, то w • v линейно независимо.

LaTeX

$$LinearIndependent R v → LinearIndependent R (w • v)$$

Lean4

theorem id_image (hs : LinearIndepOn R v s) : LinearIndepOn R id (v '' s) :=
  LinearIndepOn.image_of_comp v id hs

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

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

Разделы

Аффилиация

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