tmul_one_mul_one_tmul — Mathlib

English

Unit-based multiplication equivalence: (a ᵍ⊗ 1) * (1 ᵍ⊗ b) = a ᵍ⊗ b.

Русский

Эквивалентность умножения на единицах: (a ᵍ⊗ 1) * (1 ᵍ⊗ b) = a ᵍ⊗ b.

LaTeX

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

Lean4

theorem tmul_one_mul_one_tmul (a₁ : A) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (1 : B) * (1 : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = (a₁ : A) ᵍ⊗ₜ(b₂ : B) :=
  by
  convert tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ (GradedMonoid.GOne.one (A := (ℬ ·))) (GradedMonoid.GOne.one (A := (𝒜 ·))) b₂
  · rw [SetLike.coe_gOne, mul_one]
  · rw [SetLike.coe_gOne, one_mul]

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