Theorem Algebra.TensorProduct.mk_one_injective_of_isScalarTower

Modification history