Commit 2024-03-12 16:34 9ddaa428

View on Github →

feat(Mathlib/LinearMap/TensorProduct/RightExtactness) : generalize and add 2 thms (#11303)

  • Generalize one assumption from AddCommGroup to AddCommMonoid at one place (no modification of a proof is needed)
  • Add two lemmas that compute the range of LinearMap.rTensor and LinearMap.lTensor
  • Adjust the names of a few lemmas : rTensor.surjective becomes LinearMap.rTensor_surjective, etc.

Estimated changes

deleted theorem lTensor.surjective
deleted theorem rTensor.surjective