Theorem LinearMap.mul'_tensor

Modification history

2025-08-31 17:16

Mathlib/RingTheory/TensorProduct/Basic.lean

chore(RingTheory/TensorProduct/Basic): generalize result (#29158) …

Added LinearMap.mul'_tensor View on Github →