Theorem TensorProduct.range_map_mono

Modification history

2025-09-28 15:39
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
chore(LinearAlgebra/TensorProduct/Basic): semi-linearize `map` and `lift` (#27288) …
Modified TensorProduct.range_map_monoView on Github →
2025-09-14 23:26
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat(LinearAlgebra/TensorProduct/Basic): add `range_map_mono` (#29343)
Added TensorProduct.range_map_monoView on Github →