quotIdealMapEquivTensorQuot_symm_tmul

English

The inverse of the canonical quotient–tensor isomorphism sends a simple tensor b ⊗ a to the quotient class of a·b in B/IB.

Русский

Обратное изображение канонического изоморфизма через тензор–фактор sends простой тензор b ⊗ a в класc по идеалу IB от элемента a·b.

LaTeX

$$$(\\mathrm{quotIdealMapEquivTensorQuot}_{B,I})^{-1}(b \\otimes_A a) = \\overline{a\\,b}$$$

Lean4

@[simp]
theorem quotIdealMapEquivTensorQuot_symm_tmul (b : B) (a : A) :
    (quotIdealMapEquivTensorQuot B I).symm (b ⊗ₜ[A] a) = Submodule.Quotient.mk (a • b) :=
  rfl

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