Theorems · Theorem · ring theory

AddMonoidAlgebra.tensorEquiv_symm_single_eq_tmul_single_zero

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] (mn : M × N) (r : R),
  (AddMonoidAlgebra.tensorEquiv R).symm (AddMonoidAlgebra.single mn r) =
    AddMonoidAlgebra.single mn.1 r ⊗ₜ[R] AddMonoidAlgebra.single mn.2 1

Defined in: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Cited by: 0 results in Mathlib
Foundations: Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites18

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
RingHom.idstatement · cited by 18,349
CommSemiringstatement and proof · cited by 10,911
LinearEquivstatement · cited by 3,317
TensorProductstatement · cited by 2,545
LinearEquiv.symmstatement and proof · cited by 1,461
TensorProduct.tmulstatement and proof · cited by 1,182
Finsupp.singleproof · cited by 943
AddMonoidAlgebrastatement · cited by 649
LinearEquiv.transproof · cited by 298
AddMonoidAlgebra.singlestatement and proof · cited by 250
TensorProduct.congrproof · cited by 50

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.