Theorems · Theorem · ring theory

AddMonoidAlgebra.tensorEquiv_single_tmul_single

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] (m : M) (r₁ : R) (n : N) (r₂ : R),
  (AddMonoidAlgebra.tensorEquiv R) (AddMonoidAlgebra.single m r₁ ⊗ₜ[R] AddMonoidAlgebra.single n r₂) =
    AddMonoidAlgebra.single (m, n) (r₁ * r₂)

Defined in

Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Cited by

0 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring