congr

Mathlib.LinearAlgebra.LinearIndependent.Basic

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

English

If w ≡ v on s, then LinearIndepOn R w s holds if LinearIndepOn R v s holds.

Русский

Если w совпадает с v на s, то линейная независимость w по s следует из независимости v по s.

LaTeX

$$LinearIndepOn R w s ↔ LinearIndepOn R v s$$

Lean4

theorem congr {w : ι → M} (hli : LinearIndepOn R v s) (h : EqOn v w s) : LinearIndepOn R w s :=
  (linearIndepOn_congr h).1 hli

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

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

Разделы

Аффилиация

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