coe_prodComm

Mathlib.Geometry.Manifold.Diffeomorph

URI: https://scilib.ai/kg/mathlib#Diffeomorph.coe_prodComm

English

The coordinate map of the swapped product under product congruence is the swap of coordinates.

Русский

Координатная карта обмена на произведении равна перестановке координат.

LaTeX

$$$\text{coe_prodComm} : (h_1) \otimes (h_2) \mapsto (Prod.swap)$$$

Lean4

@[simp]
theorem coe_prodComm : ⇑(prodComm I J M N n) = Prod.swap :=
  rfl

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

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

Разделы

Аффилиация

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