vecCons_apply

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#LinearMap.vecCons_apply

English

For f: M →ₗ[R] M₂ and g: M →ₗ[R] Fin n → M₂, the value of f.vecCons g at m is Matrix.vecCons (f m) (g m).

Русский

Для f и g значение f.vecCons g в m равно Matrix.vecCons (f m) (g m).

LaTeX

$$$$ f.vecCons\\; g\\; m = \\text{Matrix.vecCons} (f\\, m) (g\\, m), $$$$

Lean4

@[simp]
theorem vecCons_apply {n} (f : M →ₗ[R] M₂) (g : M →ₗ[R] Fin n → M₂) (m : M) :
    f.vecCons g m = Matrix.vecCons (f m) (g m) :=
  rfl

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

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

Разделы

Аффилиация

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