skewProd_apply

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#LinearEquiv.skewProd_apply

English

The skewProd map acts on inputs by mapping (m, m3) to (e1 m, e2 m3 + f m).

Русский

SkewProd отображает (m, m3) в (e1 m, e2 m3 + f m).

LaTeX

$$$e_1.\mathrm{skewProd} e_2 f \; (m,m_3) = (e_1 m, e_2 m_3 + f m)$$$

Lean4

@[simp]
theorem skewProd_apply (f : M →ₗ[R] M₄) (x) : e₁.skewProd e₂ f x = (e₁ x.1, e₂ x.2 + f x.1) :=
  rfl

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

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

Разделы

Аффилиация

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