prodCongr_apply

Mathlib.LinearAlgebra.Prod

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

English

Another formulation of the symmetry of prodCongr under inverse operation.

Русский

Ещё одно выражение симметрии prodCongr при обращении.

LaTeX

$$$(e_1.\mathrm{prodCongr} e_2).\mathrm{symm} = e_1.\mathrm{symm}.prodCongr e_2.\mathrm{symm}$$$

Lean4

@[simp]
theorem prodCongr_apply (p) : e₁.prodCongr e₂ p = (e₁ p.1, e₂ p.2) :=
  rfl

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

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

Разделы

Аффилиация

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