Theorem TensorProduct.CompatibleSMul.of_algebraMap_surjective

Modification history

2026-03-17 11:40
Mathlib/LinearAlgebra/TensorProduct/Associator.lean
chore(Algebra): make `TensorProduct.equivOfCompatibleSMul` more linear (#35643)
Added TensorProduct.CompatibleSMul.of_algebraMap_surjectiveView on Github →