Commit 2024-03-29 17:32 6bd93cd5

View on Github →

feat(RingTheory/Flat/Basic): add lTensor_preserves_injective_linearMap (#11748) also move lTensor_inj_iff_rTensor_inj to LinearMap

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem LinearMap.lTensor_bij_iff_rTensor_bij

added theorem LinearMap.lTensor_inj_iff_rTensor_inj

added theorem LinearMap.lTensor_surj_iff_rTensor_surj

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem Module.Flat.iff_lTensor_preserves_injective_linearMap

deleted theorem Module.Flat.lTensor_inj_iff_rTensor_inj

added theorem Module.Flat.lTensor_preserves_injective_linearMap

deleted theorem Module.Flat.preserves_injective_linearMap

added theorem Module.Flat.rTensor_preserves_injective_linearMap