English
Product of ring isomorphisms yields a ring isomorphism on the product: given f : R ≃+* R' and g : S ≃+* S', we obtain a ring isomorphism R × S ≃+* R' × S' by applying f to the first coordinate and g to the second.
Русский
Производное по произведению кольцевых эквивалентностей дает кольцевой эквивалент на произведении: если f: R ≃+* R' и g: S ≃+* S', то существует кольцевой эквивалент R × S ≃+* R' × S', который действует координатно: (r,s) ↦ (f r, g s).
LaTeX
$$$$ (R \\times S) \\cong+* (R' \\times S') \\;\\text{via } (f,g): (r,s) \\mapsto (f r, g s). $$$$
Lean4
/-- Product of ring equivalences. This is `Equiv.prodCongr` as a `RingEquiv`. -/
@[simps!]
def prodCongr {R R' S S' : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R']
[NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') : R × S ≃+* R' × S'
where
toEquiv := Equiv.prodCongr f g
map_mul' _
_ := by simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe, Prod.map, map_mul, Prod.mk_mul_mk]
map_add' _
_ := by simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe, Prod.map, map_add, Prod.mk_add_mk]
