Mathlib Map

Theorems · Theorem · linear algebra

TensorProduct.lid_eq_rid

∀ (R : Type u_1) [inst : CommSemiring R], TensorProduct.lid R R = TensorProduct.rid R R
Defined in
Mathlib.LinearAlgebra.TensorProduct.Associator
Cited by
2 results in Mathlib
Foundations
Depth 64 from the axioms · uses propext, Quot.sound
Assumes
CommSemiring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

finsuppTensorFinsuppRid_self · cited by 0finsuppTensorFinsuppRid_s…TensorProduct.lidIsometry_eq_ridIsometry · cited by 0TensorProduct.lidIsometry…RingHom.id · cited by 18349RingHom.idCommSemiring · cited by 10911CommSemiringLinearEquiv · cited by 3317LinearEquivTensorProduct · cited by 2545TensorProductmul_comm · cited by 2262mul_commTensorProduct.lid · cited by 96TensorProduct.lidTensorProduct.rid · cited by 63TensorProduct.ridTensorProduct.ext' · cited by 39TensorProduct.ext'LinearEquiv.toLinearMap_injective · cited by 29LinearEquiv.toLinearMap_i…TensorProduct.lid_eq_ridCITED BYCITES

Cites9

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

Cited by2

Results whose statement or proof uses this declaration.