Theorem TensorProduct.AlgebraTensorModule.restrictScalars_rTensor

Modification history

2024-12-20 22:32
Mathlib/LinearAlgebra/TensorProduct/Tower.lean
feat(RingTheory/Flat): generalize `flat_of_isLocalized_span` (#19788) …
Added TensorProduct.AlgebraTensorModule.restrictScalars_rTensorView on Github →