prod — Mathlib

English

From two isomorphisms f: P≅Q and g: S≅T one obtains an isomorphism (P,S) ≅ (Q,T).

Русский

Из двух изоморфизмов f: P≅Q и g: S≅T следует изоморфизм (P,S) ≅ (Q,T).

LaTeX

$$$\text{Iso.prod}(f,g): (P,S) \cong (Q,T)$$$

Lean4

/-- Construct an isomorphism in `C × D` out of two isomorphisms in `C` and `D`. -/
@[simps]
def prod {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T) : (P, S) ≅ (Q, T)
    where
  hom := (f.hom, g.hom)
  inv := (f.inv, g.inv)

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