Theorem LinearMap.lTensor_surj_iff_rTensor_surj

Modification history

2026-02-12 09:07

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

refactor(LinearAlgebra/TensorProduct): split large file (#34798) …

Modified LinearMap.lTensor_surj_iff_rTensor_surj View on Github →

2024-03-29 17:32

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

feat(RingTheory/Flat/Basic): add `lTensor_preserves_injective_linearMap` (#11748) …

Added LinearMap.lTensor_surj_iff_rTensor_surj View on Github →