Theorem LinearMap.lid_comp_rTensor

Modification history

2025-02-27 07:23

Mathlib/LinearAlgebra/TensorProduct/Associator.lean

chore: split long file Mathlib.LinearAlgebra.TensorProduct.Basic (#22351)

Modified LinearMap.lid_comp_rTensor View on Github →

2024-03-02 17:21

Mathlib/LinearAlgebra/TensorProduct.lean

feat(RingTheory/Flat/Basic): a module is flat iff tensoring preserves injectivity of linear maps (#9120)

Added LinearMap.lid_comp_rTensor View on Github →