tensorProdEqualizer_ι — Mathlib

English

The θ-ι component of tensorProdEqualizer f g equals (tensorProd R S).map ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder).

Русский

Компонента ι равенства tensorProdEqualizer f g равна (tensorProd R S).map ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder).

LaTeX

$$$ (tensorProdEqualizer f g).\\ι = (tensorProd R S).map ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder) $$$

Lean4

@[simp]
theorem tensorProdEqualizer_ι {A B : Under R} (f g : A ⟶ B) :
    (tensorProdEqualizer f g).ι = (tensorProd R S).map ((AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder) :=
  rfl

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