map_prodComm_prod — Mathlib

English

Applying the product-commuting isomorphism to I × J yields J × I.

Русский

Применение изоморфизма, меняющего компоненты, к I × J дает J × I.

LaTeX

$$$\\operatorname{map} (\\text{RingEquiv.prodComm}) (I \\mathrm{prod} J) = J \\mathrm{prod} I$$$

Lean4

@[simp]
theorem map_prodComm_prod : map ((RingEquiv.prodComm : R × S ≃+* S × R) : R × S →+* S × R) (prod I J) = prod J I :=
  by
  refine Trans.trans (ideal_prod_eq _) ?_
  simp [map_map]

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