Theorem Algebra.TensorProduct.map_restrictScalars_comp_includeRight

Modification history

2025-03-02 22:29

Mathlib/RingTheory/TensorProduct/Basic.lean

refactor(RingTheory/TensorProduct): reorder variables to match the module version (#22444) …

Modified Algebra.TensorProduct.map_restrictScalars_comp_includeRight View on Github →

2023-08-07 16:43

Mathlib/RingTheory/TensorProduct.lean

feat(RingTheory/TensorProduct): heterogenize (#6417) …

Added Algebra.TensorProduct.map_restrictScalars_comp_includeRight View on Github →