ite_tmul — Mathlib

English

There is a convenient isScalarTower instance that ensures compatibility of scalar actions across the tensor product when R' and R are involved.

Русский

Существует удобный экземпляр isScalarTower, обеспечивающий совместимость действий скаляров при тензорном произведении, если задействованы R' и R.

LaTeX

$$$\text{isScalarTower} \; (R',R,M) \Rightarrow \text{IsScalarTower} (R',R,M) (M \otimes_R N)$$$

Lean4

theorem ite_tmul (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] :
    (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ x₂ else 0 := by split_ifs <;> simp

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