equivTensorProduct_symm_apply_tmul

English

If A is a localization of R, then the algebra tensor product over A is canonically isomorphic to the tensor product over R; i.e., B ⊗_A C ≃_A B ⊗_R C.

Русский

Если A — локализация от R, канонический тензорный произведение по A эквивалентно произведению по R: B ⊗_A C ≃_A B ⊗_R C.

LaTeX

$$$B \otimes_A C \cong_A B \otimes_R C$$$

Lean4

@[simp]
theorem equivTensorProduct_symm_apply_tmul (x : M) (r : R) (s : S) :
    (equivTensorProduct S M).symm (Localization.mk r s ⊗ₜ[R] x) = r • mk x s := by
  simp [equivTensorProduct, IsBaseChange.equiv_tmul, mk_smul_mk, smul'_mk]

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