swap — Mathlib

English

Swapping components is a continuous monoid homomorphism (A × B) →* (B × A) given by (a,b) ↦ (b,a).

Русский

Поменять модули компонентов: (A × B) →* (B × A), (a,b) ↦ (b,a).

LaTeX

$$$swap: (A \\times B) \\to_* (B \\times A)$$$

Lean4

/-- The continuous homomorphism given by swapping components. -/
@[to_additive (attr := simps!) /-- The continuous homomorphism given by swapping components. -/
    ]
def swap : (A × B) →ₜ* (B × A) :=
  prod (snd A B) (fst A B)

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