coe_prodCongr — Mathlib

English

The underlying function of RingEquiv.prodCongr f g is the Cartesian product map: it acts on a pair by applying f to the first component and g to the second.

Русский

Функциональное основание RingEquiv.prodCongr f g есть произведение: на паре (x,y) действует f на первую координату и g на вторую.

LaTeX

$$$$ \\big(\\text{RingEquiv.prodCongr } f g\\big)(x,y) = (f x, g y). $$$$

Lean4

@[simp]
theorem coe_prodCongr {R R' S S' : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R']
    [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') :
    ⇑(RingEquiv.prodCongr f g) = Prod.map f g :=
  rfl

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