skewSwap_symm_apply

Mathlib.LinearAlgebra.Prod

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

English

Reiteration of the bottom-product criterion in the additive context with maps.

Русский

Повторение условия нулевого произведения в контексте отображений.

LaTeX

$$$p_1.\mathrm{prod} p_2 = \bot \iff p_1 = \bot \land p_2 = \bot$$$

Lean4

@[simp]
theorem skewSwap_symm_apply (x : N × M) : (LinearEquiv.skewSwap R M N).symm x = (x.2, -x.1) :=
  rfl

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

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

Разделы

Аффилиация

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