tmul_one_mul_coe_tmul — Mathlib

English

Multiplication with unit expectations: (a ᵍ⊗ 1) * (1 ᵍ⊗ b) = a ᵍ⊗ b.

Русский

Умножение с единицами: (a ᵍ⊗ 1) * (1 ᵍ⊗ b) = a ᵍ⊗ b.

LaTeX

$$$(a ᵍ⊗ 1) * (1 ᵍ⊗ b) = a ᵍ⊗ b$$$

Lean4

theorem tmul_one_mul_coe_tmul {i₂ : ι} (a₁ : A) (a₂ : 𝒜 i₂) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (1 : B) * (a₂ : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = (a₁ * a₂ : A) ᵍ⊗ₜ(b₂ : B) :=
  by
  convert tmul_zero_coe_mul_coe_tmul 𝒜 ℬ a₁ (@GradedMonoid.GOne.one _ (ℬ ·) _ _) a₂ b₂
  rw [SetLike.coe_gOne, one_mul]

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