tensorEqualizerEquiv_apply — Mathlib

English

The coefficient map for tensorEqualizer commutes with the functorial map to the target tensor product.

Русский

Коэффициентное отображение tensorEqualizer коммутирует с отображением к целевому тензорному произведению.

LaTeX

$$coe_tensorEqualizer (x) = AlgHom.tensorEqualizer S T f g x$$

Lean4

@[simp]
theorem tensorEqualizerEquiv_apply [Module.Flat R T] (x : T ⊗[R] AlgHom.equalizer f g) :
    AlgHom.tensorEqualizerEquiv S T f g x = AlgHom.tensorEqualizer S T f g x :=
  rfl

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