mul_eq_tensor — Mathlib

English

The product of Pic R elements M and N corresponds to the Picard class of their tensor product: M * N = Pic.mk R (M ⊗_R N).

Русский

Произведение элементов группы Пикарда M и N соответствует классу тензорного произведения: M · N = Pic.mk R (M ⊗_R N).

LaTeX

$$$ M \\; * \\; N = \\mathrm{Pic.mk} R (M \\otimes_R N). $$$

Lean4

theorem mul_eq_tensor (M N : Pic R) : M * N = Pic.mk R (M ⊗[R] N) := by rw [mk_tensor, mk_eq_self, mk_eq_self]

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