tmul_zero_coe_mul_coe_tmul — Mathlib

English

A precise graded product formula on partially homogeneous elements: the sign is (-1)^{j1 i2} and the result is (a1 a2) ᵍ⊗ (b1 b2).

Русский

Точная формула градуированного произведения для частично однородных элементов: знак (-1)^{j1 i2} и результат (a1 a2) ᵍ⊗ (b1 b2).

LaTeX

$$$(-1)^{j_1 i_2} \cdot ((a_1 a_2) ᵍ⊗ (b_1 b_2)) = (a_1 ᵍ⊗ b_1) * (a_2 ᵍ⊗ b_2)$$$

Lean4

/-- A special case for when `b₁` has grade 0. -/
theorem tmul_zero_coe_mul_coe_tmul {i₂ : ι} (a₁ : A) (b₁ : ℬ 0) (a₂ : 𝒜 i₂) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (b₁ : B) * (a₂ : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = ((a₁ * a₂ : A) ᵍ⊗ₜ(b₁ * b₂ : B)) := by
  rw [tmul_coe_mul_coe_tmul, zero_mul, uzpow_zero, one_smul]

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