Theorem Algebra.TensorProduct.basisAux_map_smul

Modification history

2024-11-05 12:09
Mathlib/RingTheory/TensorProduct/Basic.lean
chore(RingTheory/TensorProduct): split finite/free results into new files (#18653)
Modified Algebra.TensorProduct.basisAux_map_smulView on Github →
2023-09-14 13:42
Mathlib/RingTheory/TensorProduct.lean
chore(RingTheory/TensorProduct): cleanup type names (#7145) …
Modified Algebra.TensorProduct.basisAux_map_smulView on Github →
2023-05-17 23:10
Mathlib/RingTheory/TensorProduct.lean
feat: port RingTheory.TensorProduct (#4004)
Added Algebra.TensorProduct.basisAux_map_smulView on Github →