Theorem TensorProduct.AlgebraTensorModule.mk_eq

Modification history

2026-05-25 15:44
Mathlib/LinearAlgebra/TensorProduct/Tower.lean
chore(RingTheory/TensorProduct/Basic): some API for `includeLeft` and `includeRight` (#39694)
Added TensorProduct.AlgebraTensorModule.mk_eqView on Github →