constantBaseRingEquiv_symm — Mathlib

English

The inverse of the constant base ring equivalence sends an element r ∈ R to the corresponding algebra map from R to the PiTensorProduct, i.e., it is algebraMap R (PiTensorProduct R ...).

Русский

Обратное к базовому эквиваленту отображает элемент r ∈ R в соответствующее отображение алгебры R в PiTensorProduct.

LaTeX

$$$ (constantBaseRingEquiv_{ι,R})^{-1} (r) = \\text{algebraMap}_R^{\\PiTensorProduct} (r)$$$

Lean4

@[simp]
theorem constantBaseRingEquiv_symm (r : R) : (constantBaseRingEquiv ι R).symm r = algebraMap _ _ r :=
  rfl

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