English
There exists a multiplicative equivalence between M × N and N × M given by swapping coordinates; this is the product swap isomorphism.
Русский
Существует мультипликативное эквивалентное отображение между M × N и N × M, заданное перестановкой координат; это изоморфизм обмена.
LaTeX
$$prodComm : M × N ≃* N × M$$
Lean4
/-- The equivalence between `M × N` and `N × M` given by swapping the components
is multiplicative. -/
@[to_additive prodComm /-- The equivalence between `M × N` and `N × M` given by swapping the
components is additive. -/
]
def prodComm : M × N ≃* N × M :=
{ Equiv.prodComm M N with map_mul' := fun ⟨_, _⟩ ⟨_, _⟩ => rfl }
