Theorem Subalgebra.rTensorBot_symm_apply

Modification history

2024-07-16 22:33
Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean
feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras (#14611) …
Added Subalgebra.rTensorBot_symm_applyView on Github →