snd_linear

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.snd_linear

English

The linear part of snd is the second-coordinate projection on the vector components.

Русский

Линейная часть snd — это проекция на вторую координату в векторной части.

LaTeX

$$$\\mathrm{snd.linear} = \\mathrm{LinearMap.snd}_{k,V_1,V_2}$$$

Lean4

@[simp]
theorem snd_linear : (snd : P1 × P2 →ᵃ[k] P2).linear = LinearMap.snd k V1 V2 :=
  rfl

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

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

Разделы

Аффилиация

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