Theorem TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange

Modification history

2025-01-02 11:03
Mathlib/LinearAlgebra/TensorProduct/Tower.lean
feat(Algebra): auxiliary lemmas for flatness over semirings (#20265)
Added TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChangeView on Github →